Final

📁 Source: Mathlib/Order/Interval/Set/Final.lean

Statistics

Metric	Count
Definitions	0
Theorems subtype_functor_final	1
Total	1

Set.Ici

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subtype_functor_final 📖	mathematical	—	CategoryTheory.Functor.Final Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.smallCategory Subtype.preorder Monotone.functor Subtype.mono_coe	—	Subtype.mono_coe Monotone.final_functor_iff SemilatticeSup.instIsDirectedOrder le_max_left le_max_right

---

← Back to Index