Documentation
Mathlib
.
Order
.
Interval
.
Set
.
Final
Search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Filtered.Final
Imported by
Set
.
Ici
.
subtype_functor_final
Final functors betwen intervals
#
source
instance
Set
.
Ici
.
subtype_functor_final
{J :
Type
u}
[
LinearOrder
J
]
(j :
J
)
:
⋯
.
functor
.
Final