Intervals

📁 Source: Mathlib/Order/CompactlyGenerated/Intervals.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsCompactlyGenerated, isCompactElement, complementedLattice_of_complementedLattice_Iic	3
Total	3

Set.Iic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCompactlyGenerated 📖	mathematical	—	IsCompactlyGenerated Set.Elem Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	IsCompactlyGenerated.exists_sSup_eq sSup_le_iff isCompactElement Set.ext
isCompactElement 📖	mathematical	IsCompactElement ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set Set.instMembership Set.Iic PartialOrder.toPreorder	Set.Elem Subtype.partialOrder	—	Finset.sup_eq_iSup le_trans le_refl coe_iSup iSup_congr_Prop

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complementedLattice_of_complementedLattice_Iic 📖	—	ComplementedLattice Set.Elem Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set.Iic.instLatticeElem ConditionallyCompleteLattice.toLattice Set.Iic.instBoundedOrderElemOfOrderBot BoundedOrder.toOrderBot Preorder.toLE CompleteLattice.toBoundedOrder iSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop	—	—	complementedLattice_of_sSup_atoms_eq_top complementedLattice_iff_isAtomistic IsModularLattice.isModularLattice_Iic Set.Iic.instIsCompactlyGenerated eq_sSup_atoms IsAtom.of_isAtom_coe_Iic sSup_iUnion biSup_congr' eq_top_iff sSup_le_sSup

---

← Back to Index