Documentation Verification Report

Cofinal

📁 Source: Mathlib/Order/Cofinal.lean

Statistics

Metric	Count
Definitions `Cofinal`, `instInhabitedSubtypeSetIsCofinal`	2
Theorems `of_not_isCofinal`, `isCofinal_range`, `map_cofinal`, `map_isCofinal`, `image`, `mem_of_isMax`, `mono`, `of_isEmpty`, `of_not_bddAbove`, `singleton_top`, `top_mem`, `trans`, `univ`, `map_cofinal`, `map_isCofinal`, `map_isCofinal_iff`, `isCofinal_empty_iff`, `isCofinal_iff_iUnion_Iic_eq_univ`, `isCofinal_iff_iUnion_Iio_eq_univ`, `isCofinal_iff_top_mem`, `isCofinal_setOf_imp_lt`, `isCofinal_singleton_iff`, `not_bddAbove_iff_isCofinal`, `not_isCofinal_iff`, `not_isCofinal_iff_bddAbove`	25
Total	27

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_not_isCofinal` 📖	mathematical	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`not_isCofinal_iff` `LT.lt.le`

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCofinal_range` 📖	mathematical	`GaloisConnection`	`IsCofinal` `Preorder.toLE` `Set.range`	—	`Set.mem_range_self` `le_u_l`
`map_cofinal` 📖	mathematical	`GaloisConnection` `IsCofinal` `Preorder.toLE`	`IsCofinal` `Preorder.toLE` `Set.image`	—	`map_isCofinal`
`map_isCofinal` 📖	mathematical	`GaloisConnection` `IsCofinal` `Preorder.toLE`	`IsCofinal` `Preorder.toLE` `Set.image`	—	`IsCofinal.image` `monotone_u` `isCofinal_range`

IsCofinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image` 📖	mathematical	`IsCofinal` `Preorder.toLE` `Monotone` `Set.range`	`IsCofinal` `Preorder.toLE` `Set.image`	—	`Set.mem_image_of_mem` `LE.le.trans`
`mem_of_isMax` 📖	mathematical	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `IsCofinal`	`Set` `Set.instMembership`	—	`IsMax.eq_of_ge`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `IsCofinal`	`IsCofinal`	—	—
`of_isEmpty` 📖	mathematical	—	`IsCofinal`	—	—
`of_not_bddAbove` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `BddAbove.of_not_isCofinal`
`singleton_top` 📖	mathematical	—	`IsCofinal` `Set` `Set.instSingletonSet` `Top.top` `OrderTop.toTop`	—	—
`top_mem` 📖	mathematical	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`mem_of_isMax` `isMax_top`
`trans` 📖	mathematical	`IsCofinal` `Preorder.toLE` `Set.Elem` `Set` `Set.instMembership`	`IsCofinal` `Preorder.toLE` `Set.image` `Set` `Set.instMembership`	—	`image` `Subtype.mono_coe` `Subtype.range_coe_subtype`
`univ` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `Set.univ`	—	`le_rfl`

Order

Definitions

Name	Category	Theorems
`Cofinal` 📖	CompData	3 math math: `Cofinal.above_mem`, `cofinal_meets_idealOfCofinals`, `sequenceOfCofinals.encode_mem`

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_cofinal` 📖	mathematical	`IsCofinal` `Preorder.toLE`	`IsCofinal` `Preorder.toLE` `Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`map_isCofinal`
`map_isCofinal` 📖	mathematical	`IsCofinal` `Preorder.toLE`	`IsCofinal` `Preorder.toLE` `Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`GaloisConnection.map_isCofinal` `to_galoisConnection`
`map_isCofinal_iff` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`symm_image_image` `map_isCofinal`

(root)

Definitions

Name	Category	Theorems
`instInhabitedSubtypeSetIsCofinal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCofinal_empty_iff` 📖	mathematical	—	`IsCofinal` `Set` `Set.instEmptyCollection` `IsEmpty`	—	`IsCofinal.of_isEmpty`
`isCofinal_iff_iUnion_Iic_eq_univ` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `Set.iUnion` `Set` `Set.instMembership` `Set.Iic` `Set.univ`	—	—
`isCofinal_iff_iUnion_Iio_eq_univ` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `Set.iUnion` `Set` `Set.instMembership` `Set.Iio` `Set.univ`	—	`NoMaxOrder.exists_gt` `LT.lt.trans_le` `isCofinal_iff_iUnion_Iic_eq_univ` `Set.univ_subset_iff` `Set.iUnion_mono''` `Set.Iio_subset_Iic_self`
`isCofinal_iff_top_mem` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership` `Top.top` `OrderTop.toTop`	—	`IsCofinal.top_mem` `le_top`
`isCofinal_setOf_imp_lt` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `setOf`	—	`WellFounded.has_min` `IsWellFounded.wf` `Set.nonempty_Ici` `LE.le.trans`
`isCofinal_singleton_iff` 📖	mathematical	—	`IsCofinal` `Set` `Set.instSingletonSet` `IsTop`	—	—
`not_bddAbove_iff_isCofinal` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsCofinal`	—	`not_iff_comm` `not_isCofinal_iff_bddAbove`
`not_isCofinal_iff` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT`	—	—
`not_isCofinal_iff_bddAbove` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BddAbove`	—	`BddAbove.of_not_isCofinal` `not_isCofinal_iff` `NoMaxOrder.exists_gt` `LE.le.trans_lt`

---

← Back to Index