Cofinal

📁 Source: Mathlib/Order/Cofinal.lean

Statistics

Metric	Count
Definitions Cofinal, instInhabitedSubtypeSetIsCofinal	2
Theorems of_not_isCofinal, map_cofinal, mem_of_isMax, mono, of_isEmpty, of_not_bddAbove, singleton_top, top_mem, trans, univ, map_cofinal, isCofinal_empty_iff, isCofinal_iff_top_mem, isCofinal_setOf_imp_lt, not_bddAbove_iff_isCofinal, not_isCofinal_iff, not_isCofinal_iff_bddAbove	17
Total	19

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	—	not_isCofinal_iff LT.lt.le

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_cofinal 📖	mathematical	GaloisConnection IsCofinal Preorder.toLE	Set.image	—	Set.mem_image_of_mem le_iff_le

IsCofinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_of_isMax 📖	mathematical	IsMax Preorder.toLE PartialOrder.toPreorder IsCofinal	Set Set.instMembership	—	IsMax.eq_of_ge
mono 📖	—	Set Set.instHasSubset IsCofinal	—	—	—
of_isEmpty 📖	mathematical	—	IsCofinal	—	—
of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsCofinal	—	Mathlib.Tactic.Contrapose.contrapose₂ BddAbove.of_not_isCofinal
singleton_top 📖	mathematical	—	IsCofinal Set Set.instSingletonSet Top.top OrderTop.toTop	—	Set.mem_singleton le_top
top_mem 📖	mathematical	IsCofinal Preorder.toLE PartialOrder.toPreorder	Set Set.instMembership Top.top OrderTop.toTop	—	mem_of_isMax isMax_top
trans 📖	mathematical	IsCofinal Preorder.toLE Set.Elem Set Set.instMembership	Set.image	—	Set.mem_image_of_mem LE.le.trans
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	Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	GaloisConnection.map_cofinal to_galoisConnection

(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_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
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