Ideal

Statistics

Metric	Count
Definitions `above`, `carrier`, `instInhabited`, `instMembership`, `Ideal`, `IsMaximal`, `IsProper`, `instCompleteLattice`, `instInfSet`, `instInhabited`, `instLattice`, `instMax`, `instMin`, `instOrderBot`, `instOrderTop`, `instPartialOrder`, `instPartialOrderIdeal`, `instSetLike`, `principal`, `toLowerSet`, `IsIdeal`, `toIdeal`, `idealOfCofinals`, `sequenceOfCofinals`	24
Theorems `isMaximal`, `isProper`, `above_mem`, `isCofinal`, `le_above`, `isCoatom`, `isCoatom'`, `maximal_proper`, `toIsProper`, `ne_top`, `ne_univ`, `notMem_of_compl_mem`, `notMem_or_compl_notMem`, `top_notMem`, `bot_mem`, `carrier_eq_coe`, `coe_inf`, `coe_sInf`, `coe_ssubset_coe`, `coe_subset_coe`, `coe_sup`, `coe_sup_eq`, `coe_toLowerSet`, `coe_top`, `directed`, `directed'`, `eq_sup_of_le_sup`, `ext`, `ext_iff`, `finsetSup_mem_iff`, `inter_nonempty`, `isIdeal`, `isMaximal_iff`, `isMaximal_iff_isCoatom`, `isProper_iff`, `isProper_iff_ne_top`, `isProper_of_ne_top`, `isProper_of_notMem`, `lower`, `lt_sup_principal_of_notMem`, `mem_compl_of_ge`, `mem_inf`, `mem_of_mem_of_le`, `mem_principal`, `mem_principal_self`, `mem_sInf`, `mem_sup`, `nonempty`, `nonempty'`, `principal_bot`, `principal_le_iff`, `principal_toLowerSet`, `principal_top`, `sup_mem`, `sup_mem_iff`, `toLowerSet_injective`, `top_of_top_mem`, `top_toLowerSet`, `IsLowerSet`, `cofinal_meets_idealOfCofinals`, `isIdeal_iff`, `isIdeal_sUnion_of_directedOn`, `isIdeal_sUnion_of_isChain`, `mem_idealOfCofinals`, `encode_mem`, `monotone`	66
Total	90

IsCoatom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal` 📖	mathematical	`IsCoatom` `Order.Ideal` `PartialOrder.toPreorder` `Order.Ideal.instPartialOrderIdeal` `Order.Ideal.instOrderTop`	`Order.Ideal.IsMaximal`	—	`isProper`
`isProper` 📖	mathematical	`IsCoatom` `Order.Ideal` `PartialOrder.toPreorder` `Order.Ideal.instPartialOrderIdeal` `Order.Ideal.instOrderTop`	`Order.Ideal.IsProper`	—	`Order.Ideal.isProper_of_ne_top`

Order

Definitions

Name	Category	Theorems
`Ideal` 📖	CompData	49 math math: `Ideal.PrimePair.I_union_F`, `Ideal.ext_iff`, `mem_idealOfCofinals`, `Ideal.lower`, `Ideal.isPrime_iff`, `Ideal.IsProper.notMem_or_compl_notMem`, `Ideal.coe_sup`, `Ideal.principal_bot`, `Ideal.toLowerSet_injective`, `Ideal.coe_sup_eq`, `Ideal.IsProper.top_notMem`, `Ideal.isMaximal_iff_isCoatom`, `Ideal.IsPrime.compl_filter`, `Ideal.PrimePair.isCompl_I_F`, `Ideal.PrimePair.compl_I_eq_F`, `Ideal.directed`, `Ideal.isPrime_iff_mem_or_compl_mem`, `Ideal.mem_principal_self`, `Ideal.mem_principal`, `Ideal.top_toLowerSet`, `Ideal.IsMaximal.isCoatom'`, `Ideal.carrier_eq_coe`, `Ideal.principal_le_iff`, `PFilter.mem_mk`, `Ideal.inter_nonempty`, `Ideal.nonempty`, `cofinal_meets_idealOfCofinals`, `Ideal.coe_subset_coe`, `Ideal.bot_mem`, `Ideal.PrimePair.F_union_I`, `Ideal.mem_sup`, `Ideal.isMaximal_iff`, `Ideal.mem_sInf`, `Ideal.coe_inf`, `Ideal.sup_mem_iff`, `Ideal.finsetSup_mem_iff`, `Ideal.coe_top`, `Ideal.isIdeal`, `Ideal.mem_inf`, `Ideal.PrimePair.disjoint`, `Ideal.coe_ssubset_coe`, `Ideal.coe_toLowerSet`, `Ideal.IsMaximal.isCoatom`, `Ideal.PrimePair.compl_F_eq_I`, `Ideal.coe_sInf`, `DistribLattice.mem_ideal_sup_principal`, `Ideal.isPrime_iff_mem_or_mem`, `Ideal.IsPrime.mem_or_compl_mem`, `Ideal.principal_top`
`IsIdeal` 📖	CompData	4 math math: `PFilter.IsPrime.compl_ideal`, `PFilter.isPrime_iff`, `isIdeal_iff`, `Ideal.isIdeal`
`idealOfCofinals` 📖	CompOp	2 math math: `mem_idealOfCofinals`, `cofinal_meets_idealOfCofinals`
`sequenceOfCofinals` 📖	CompOp	2 math math: `sequenceOfCofinals.monotone`, `sequenceOfCofinals.encode_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cofinal_meets_idealOfCofinals` 📖	mathematical	—	`Cofinal` `Cofinal.instMembership` `Ideal` `Preorder.toLE` `SetLike.instMembership` `Ideal.instSetLike` `idealOfCofinals`	—	`sequenceOfCofinals.encode_mem` `le_rfl`
`isIdeal_iff` 📖	mathematical	—	`IsIdeal` `IsLowerSet` `Set.Nonempty` `DirectedOn`	—	—
`isIdeal_sUnion_of_directedOn` 📖	mathematical	`IsIdeal` `Preorder.toLE` `DirectedOn` `Set` `Set.instHasSubset` `Set.Nonempty`	`Set.sUnion`	—	`isLowerSet_sUnion` `IsIdeal.IsLowerSet` `Set.nonempty_sUnion` `IsIdeal.Nonempty` `Set.directedOn_sUnion` `IsIdeal.Directed`
`isIdeal_sUnion_of_isChain` 📖	mathematical	`IsIdeal` `Preorder.toLE` `IsChain` `Set` `Set.instHasSubset` `Set.Nonempty`	`Set.sUnion`	—	`isIdeal_sUnion_of_directedOn` `IsChain.directedOn` `Set.instReflSubset`
`mem_idealOfCofinals` 📖	mathematical	—	`Ideal` `Preorder.toLE` `SetLike.instMembership` `Ideal.instSetLike` `idealOfCofinals`	—	`le_rfl`

Order.Cofinal

Definitions

Name	Category	Theorems
`above` 📖	CompOp	2 math math: `above_mem`, `le_above`
`carrier` 📖	CompOp	1 math math: `isCofinal`
`instInhabited` 📖	CompOp	—
`instMembership` 📖	CompOp	3 math math: `above_mem`, `Order.cofinal_meets_idealOfCofinals`, `Order.sequenceOfCofinals.encode_mem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`above_mem` 📖	mathematical	—	`Order.Cofinal` `instMembership` `above`	—	`isCofinal`
`isCofinal` 📖	mathematical	—	`IsCofinal` `Preorder.toLE` `carrier`	—	—
`le_above` 📖	mathematical	—	`Preorder.toLE` `above`	—	`isCofinal`

Order.Ideal

Definitions

Name	Category	Theorems
`IsMaximal` 📖	CompData	4 math math: `isMaximal_iff_isCoatom`, `IsCoatom.isMaximal`, `isMaximal_iff`, `IsPrime.isMaximal`
`IsProper` 📖	CompData	10 math math: `IsMaximal.toIsProper`, `IsCoatom.isProper`, `IsPrime.toIsProper`, `isPrime_iff`, `isProper_iff`, `isProper_iff_ne_top`, `isProper_of_ne_top`, `PrimePair.I_isProper`, `isMaximal_iff`, `isProper_of_notMem`
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	2 math math: `mem_sInf`, `coe_sInf`
`instInhabited` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	5 math math: `coe_sup`, `lt_sup_principal_of_notMem`, `coe_sup_eq`, `mem_sup`, `DistribLattice.mem_ideal_sup_principal`
`instMin` 📖	CompOp	2 math math: `coe_inf`, `mem_inf`
`instOrderBot` 📖	CompOp	1 math math: `principal_bot`
`instOrderTop` 📖	CompOp	7 math math: `isMaximal_iff_isCoatom`, `top_toLowerSet`, `IsMaximal.isCoatom'`, `top_of_top_mem`, `coe_top`, `IsMaximal.isCoatom`, `principal_top`
`instPartialOrder` 📖	CompOp	—
`instPartialOrderIdeal` 📖	CompOp	13 math math: `principal_bot`, `lt_sup_principal_of_notMem`, `isMaximal_iff_isCoatom`, `DistribLattice.prime_ideal_of_disjoint_filter_ideal`, `top_toLowerSet`, `IsMaximal.isCoatom'`, `principal_le_iff`, `coe_subset_coe`, `top_of_top_mem`, `coe_top`, `coe_ssubset_coe`, `IsMaximal.isCoatom`, `principal_top`
`instSetLike` 📖	CompOp	43 math math: `PrimePair.I_union_F`, `ext_iff`, `Order.mem_idealOfCofinals`, `lower`, `isPrime_iff`, `IsProper.notMem_or_compl_notMem`, `coe_sup`, `coe_sup_eq`, `IsProper.top_notMem`, `IsPrime.compl_filter`, `PrimePair.isCompl_I_F`, `IsMaximal.maximal_proper`, `PrimePair.compl_I_eq_F`, `directed`, `isPrime_iff_mem_or_compl_mem`, `mem_principal_self`, `mem_principal`, `carrier_eq_coe`, `principal_le_iff`, `Order.PFilter.mem_mk`, `inter_nonempty`, `nonempty`, `Order.cofinal_meets_idealOfCofinals`, `coe_subset_coe`, `bot_mem`, `PrimePair.F_union_I`, `mem_sup`, `isMaximal_iff`, `mem_sInf`, `coe_inf`, `sup_mem_iff`, `finsetSup_mem_iff`, `coe_top`, `isIdeal`, `mem_inf`, `PrimePair.disjoint`, `coe_ssubset_coe`, `coe_toLowerSet`, `PrimePair.compl_F_eq_I`, `coe_sInf`, `DistribLattice.mem_ideal_sup_principal`, `isPrime_iff_mem_or_mem`, `IsPrime.mem_or_compl_mem`
`principal` 📖	CompOp	8 math math: `principal_bot`, `principal_toLowerSet`, `lt_sup_principal_of_notMem`, `mem_principal_self`, `mem_principal`, `principal_le_iff`, `DistribLattice.mem_ideal_sup_principal`, `principal_top`
`toLowerSet` 📖	CompOp	7 math math: `directed'`, `toLowerSet_injective`, `principal_toLowerSet`, `nonempty'`, `top_toLowerSet`, `carrier_eq_coe`, `coe_toLowerSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_mem` 📖	mathematical	—	`Order.Ideal` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot`	—	`lower` `nonempty'` `bot_le` `Set.Nonempty.some_mem`
`carrier_eq_coe` 📖	mathematical	—	`LowerSet.carrier` `toLowerSet` `SetLike.coe` `Order.Ideal` `instSetLike`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	`LowerSet.coe_iInf₂`
`coe_ssubset_coe` 📖	mathematical	—	`Set` `Set.instHasSSubset` `SetLike.coe` `Order.Ideal` `instSetLike` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderIdeal`	—	—
`coe_subset_coe` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Order.Ideal` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instSetLike` `instMax` `setOf` `SetLike.instMembership` `SemilatticeSup.toMax`	—	—
`coe_sup_eq` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instSetLike` `instMax` `Lattice.toSemilatticeSup` `SemilatticeInf.instIsCodirectedOrder` `setOf` `SetLike.instMembership` `SemilatticeSup.toMax`	—	`Set.ext` `SemilatticeInf.instIsCodirectedOrder` `eq_sup_of_le_sup` `le_of_eq`
`coe_toLowerSet` 📖	mathematical	—	`SetLike.coe` `LowerSet` `LowerSet.instSetLike` `toLowerSet` `Order.Ideal` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderTop` `Set.univ`	—	—
`directed` 📖	mathematical	—	`DirectedOn` `SetLike.coe` `Order.Ideal` `instSetLike`	—	`directed'`
`directed'` 📖	mathematical	—	`DirectedOn` `LowerSet.carrier` `toLowerSet`	—	—
`eq_sup_of_le_sup` 📖	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—	`lower` `inf_le_right` `left_eq_inf` `inf_sup_left`
`ext` 📖	—	`SetLike.coe` `Order.Ideal` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `Order.Ideal` `instSetLike`	—	`ext`
`finsetSup_mem_iff` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike` `Finset.sup`	—	`Finset.induction_on` `Finset.sup_empty` `instIsEmptyFalse` `Finset.sup_insert`
`inter_nonempty` 📖	mathematical	—	`Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `Order.Ideal` `instSetLike`	—	`nonempty` `exists_le_le` `lower`
`isIdeal` 📖	mathematical	—	`Order.IsIdeal` `SetLike.coe` `Order.Ideal` `instSetLike`	—	`lower` `nonempty` `directed`
`isMaximal_iff` 📖	mathematical	—	`IsMaximal` `IsProper` `SetLike.coe` `Order.Ideal` `instSetLike` `Set.univ`	—	—
`isMaximal_iff_isCoatom` 📖	mathematical	—	`IsMaximal` `IsCoatom` `Order.Ideal` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderTop`	—	`IsMaximal.isCoatom` `IsCoatom.isMaximal`
`isProper_iff` 📖	mathematical	—	`IsProper`	—	—
`isProper_iff_ne_top` 📖	mathematical	—	`IsProper`	—	`IsProper.ne_top` `isProper_of_ne_top`
`isProper_of_ne_top` 📖	mathematical	—	`IsProper`	—	`ext`
`isProper_of_notMem` 📖	mathematical	`Order.Ideal` `SetLike.instMembership` `instSetLike`	`IsProper`	—	`Set.mem_univ`
`lower` 📖	mathematical	—	`IsLowerSet` `SetLike.coe` `Order.Ideal` `instSetLike`	—	`LowerSet.lower'`
`lt_sup_principal_of_notMem` 📖	mathematical	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike`	`Preorder.toLT` `instPartialOrderIdeal` `instMax` `principal`	—	`LE.le.lt_of_ne` `le_sup_left`
`mem_compl_of_ge` 📖	—	`Set` `Set.instMembership` `Compl.compl` `Set.instCompl` `SetLike.coe` `Order.Ideal` `instSetLike`	—	—	`lower`
`mem_inf` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_of_mem_of_le` 📖	—	`Order.Ideal` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal`	—	—	`Set.mem_of_mem_of_subset`
`mem_principal` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `principal`	—	—
`mem_principal_self` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `principal`	—	`mem_principal` `le_refl`
`mem_sInf` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`coe_sInf`
`mem_sup` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike` `instMax` `SemilatticeSup.toMax`	—	—
`nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `Order.Ideal` `instSetLike`	—	`nonempty'`
`nonempty'` 📖	mathematical	—	`Set.Nonempty` `LowerSet.carrier` `toLowerSet`	—	—
`principal_bot` 📖	mathematical	—	`principal` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `Order.Ideal` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderBot`	—	—
`principal_le_iff` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal` `principal` `SetLike.instMembership` `instSetLike`	—	`le_rfl` `lower`
`principal_toLowerSet` 📖	mathematical	—	`toLowerSet` `Preorder.toLE` `principal` `LowerSet.Iic`	—	—
`principal_top` 📖	mathematical	—	`principal` `Top.top` `OrderTop.toTop` `Preorder.toLE` `Order.Ideal` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderTop` `OrderTop.instIsDirectedOrder` `top_nonempty`	—	`toLowerSet_injective` `OrderTop.instIsDirectedOrder` `top_nonempty` `LowerSet.Iic_top`
`sup_mem` 📖	mathematical	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike`	`SemilatticeSup.toMax`	—	`directed` `lower` `sup_le`
`sup_mem_iff` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax`	—	`lower` `le_sup_left` `le_sup_right` `sup_mem`
`toLowerSet_injective` 📖	mathematical	—	`Order.Ideal` `LowerSet` `toLowerSet`	—	—
`top_of_top_mem` 📖	mathematical	`Order.Ideal` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop`	`Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderTop` `OrderTop.instIsDirectedOrder` `top_nonempty`	—	`ext` `OrderTop.instIsDirectedOrder` `top_nonempty` `Set.ext` `lower` `le_top`
`top_toLowerSet` 📖	mathematical	—	`toLowerSet` `Top.top` `Order.Ideal` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderIdeal` `instOrderTop` `LowerSet` `LowerSet.instTop`	—	—

Order.Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoatom` 📖	mathematical	—	`IsCoatom` `Order.Ideal` `PartialOrder.toPreorder` `Order.Ideal.instPartialOrderIdeal` `Order.Ideal.instOrderTop`	—	`Order.Ideal.IsProper.ne_top` `toIsProper` `Order.Ideal.ext` `maximal_proper`
`isCoatom'` 📖	mathematical	—	`IsCoatom` `Order.Ideal` `PartialOrder.toPreorder` `Order.Ideal.instPartialOrderIdeal` `Order.Ideal.instOrderTop`	—	`isCoatom`
`maximal_proper` 📖	mathematical	`Order.Ideal` `Preorder.toLT` `PartialOrder.toPreorder` `Order.Ideal.instPartialOrderIdeal`	`SetLike.coe` `Order.Ideal.instSetLike` `Set.univ`	—	—
`toIsProper` 📖	mathematical	—	`Order.Ideal.IsProper`	—	—

Order.Ideal.IsProper

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne_top` 📖	—	—	—	—	`ne_univ`
`ne_univ` 📖	—	—	—	—	—
`notMem_of_compl_mem` 📖	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.instMembership` `Order.Ideal.instSetLike` `Compl.compl` `BooleanAlgebra.toCompl`	—	—	`top_notMem` `Order.Ideal.sup_mem` `sup_compl_eq_top`
`notMem_or_compl_notMem` 📖	mathematical	—	`Order.Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `SetLike.instMembership` `Order.Ideal.instSetLike` `Compl.compl` `BooleanAlgebra.toCompl`	—	`notMem_of_compl_mem`
`top_notMem` 📖	mathematical	—	`Order.Ideal` `SetLike.instMembership` `Order.Ideal.instSetLike` `Top.top` `OrderTop.toTop`	—	`ne_top` `OrderTop.instIsDirectedOrder` `top_nonempty` `Order.Ideal.top_of_top_mem`

Order.IsIdeal

Definitions

Name	Category	Theorems
`toIdeal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsLowerSet` 📖	mathematical	`Order.IsIdeal`	`IsLowerSet`	—	—

Order.sequenceOfCofinals

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`encode_mem` 📖	mathematical	—	`Order.Cofinal` `Order.Cofinal.instMembership` `Order.sequenceOfCofinals` `Encodable.encode`	—	`Encodable.encodek` `Order.Cofinal.above_mem`
`monotone` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `Order.sequenceOfCofinals`	—	`monotone_nat_of_le_succ` `le_refl` `Order.Cofinal.le_above`

---

← Back to Index