Showing changes from revision #3 to #4:
Added | Removed | Changed
For every type and subtype , let be a function from the subtype to . Given any subtype , the inverse image by definition is a subtype of and thus a subtype of . One could restrict the domain of to and the codomain of to , and find the inverse image of under , or the 2-fold iterated inverse image of under :
One could repeat this definition indefinitely, which could be formalised by the dependent types representing the -fold iterated inverse image of under .
Last revised on June 17, 2022 at 22:47:06. See the history of this page for a list of all contributions to it.