Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsSupClosedCompact`, `IsSupFiniteCompact`, `IsCompactElement`, `IsCompactlyGenerated`	4
Theorems `Iic_coatomic_of_compact_element`, `directed_sSup_lt_of_lt`, `exists_finset_of_le_iSup`, `isSupFiniteCompact`, `wellFoundedGT`, `isSupClosedCompact`, `wellFoundedGT`, `isSupClosedCompact`, `isSupFiniteCompact`, `coatomic_of_top_compact`, `isCompactElement_finsetSup`, `isCompactElement_iff_exists_le_iSup_of_le_iSup`, `isCompactElement_iff_exists_le_sSup_of_le_sSup`, `isCompactElement_iff_le_of_directed_sSup_le`, `isCompactlyGenerated_of_wellFoundedGT`, `isSupClosedCompact_iff_wellFoundedGT`, `isSupFiniteCompact_iff_all_elements_compact`, `isSupFiniteCompact_iff_isSupClosedCompact`, `wellFoundedGT_characterisations`, `wellFoundedGT_iff_isSupFiniteCompact`, `disjoint_iSup_left`, `disjoint_iSup_right`, `iSup_inf_eq`, `inf_iSup_eq`, `disjoint_sSup_left`, `disjoint_sSup_right`, `inf_sSup_eq`, `sSup_inf_eq`, `exists_sSup_eq`, `finite_ne_bot_of_iSupIndep`, `finite_of_iSupIndep`, `finite_of_sSupIndep`, `finite_ne_bot_of_iSupIndep`, `finite_of_iSupIndep`, `finite_of_sSupIndep`, `complementedLattice_iff_isAtomistic`, `complementedLattice_of_isAtomistic`, `complementedLattice_of_sSup_atoms_eq_top`, `exists_sSupIndep_disjoint_sSup_atoms`, `exists_sSupIndep_isCompl_sSup_atoms`, `exists_sSupIndep_of_sSup_atoms`, `exists_sSupIndep_of_sSup_atoms_eq_top`, `iInf`, `iSupIndep_iff_supIndep_of_injOn`, `iSupIndep_sUnion_of_directed`, `inf_sSup_eq_iSup_inf_sup_finset`, `isAtomic_of_complementedLattice`, `isAtomistic_of_complementedLattice`, `le_iff_compact_le_imp`, `sSupIndep_iUnion_of_directed`, `sSupIndep_iff_finite`, `sSup_compact_eq_top`, `sSup_compact_le_eq`	53
Total	57

CompleteLattice

Definitions

Name	Category	Theorems
`IsSupClosedCompact` 📖	MathDef	5 math math: `WellFoundedGT.isSupClosedCompact`, `isSupFiniteCompact_iff_isSupClosedCompact`, `isSupClosedCompact_iff_wellFoundedGT`, `IsSupFiniteCompact.isSupClosedCompact`, `wellFoundedGT_characterisations`
`IsSupFiniteCompact` 📖	MathDef	6 math math: `IsSupClosedCompact.isSupFiniteCompact`, `WellFoundedGT.isSupFiniteCompact`, `wellFoundedGT_iff_isSupFiniteCompact`, `isSupFiniteCompact_iff_isSupClosedCompact`, `isSupFiniteCompact_iff_all_elements_compact`, `wellFoundedGT_characterisations`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Iic_coatomic_of_compact_element` 📖	mathematical	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice`	`IsCoatomic` `Set.Elem` `Set.Iic` `PartialOrder.toPreorder` `Subtype.partialOrder` `Set` `Set.instMembership` `Set.Iic.orderTop`	—	`eq_or_ne` `zorn_le_nonempty₀` `IsCompactElement.directed_sSup_lt_of_lt` `IsChain.directedOn` `instReflLe` `le_sSup` `lt_of_le_of_ne` `Set.not_nonempty_iff_eq_empty` `bot_nonempty` `le_of_lt` `Maximal.prop` `ne_of_lt` `by_contradiction` `Maximal.eq_of_le` `LT.lt.le` `lt_irrefl`
`coatomic_of_top_compact` 📖	mathematical	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `toLattice` `BoundedOrder.toOrderTop` `toBoundedOrder`	`IsCoatomic`	—	`OrderIso.isCoatomic_iff` `Iic_coatomic_of_compact_element`
`isCompactElement_finsetSup` 📖	mathematical	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice`	`Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `toBoundedOrder`	—	`Finset.sup_image` `Finset.sup_le_of_le_directed` `Finset.mem_image` `le_trans` `Finset.le_sup`
`isCompactElement_iff_exists_le_iSup_of_le_iSup` 📖	mathematical	—	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `BoundedOrder.toOrderBot` `SemilatticeSup.toPartialOrder` `toBoundedOrder`	—	`isCompactElement_iff_exists_le_sSup_of_le_sSup` `Subtype.prop` `LE.le.trans` `Finset.sup_le_iff` `Finset.le_sup` `Finset.mem_image_of_mem` `Finset.mem_univ` `Subtype.range_coe` `Finset.coe_image` `Subtype.coe_preimage_self`
`isCompactElement_iff_exists_le_sSup_of_le_sSup` 📖	mathematical	—	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `BoundedOrder.toOrderBot` `SemilatticeSup.toPartialOrder` `toBoundedOrder`	—	`isCompactElement_iff_le_of_directed_sSup_le` `Finset.coe_union` `Finset.sup_union` `sSup_le_sSup` `Finset.coe_singleton` `Finset.sup_singleton` `Finset.coe_empty` `Finset.sup_empty` `Set.nonempty_of_mem` `le_trans` `le_rfl` `Finset.sup_le_of_le_directed`
`isCompactElement_iff_le_of_directed_sSup_le` 📖	mathematical	—	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder`	—	`isLUB_sSup` `isLUB_iff_sSup_eq`
`isCompactlyGenerated_of_wellFoundedGT` 📖	mathematical	—	`IsCompactlyGenerated`	—	`isSupFiniteCompact_iff_all_elements_compact` `wellFoundedGT_iff_isSupFiniteCompact` `sSup_singleton`
`isSupClosedCompact_iff_wellFoundedGT` 📖	mathematical	—	`IsSupClosedCompact` `WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice`	—	`List.TFAE.out` `wellFoundedGT_characterisations`
`isSupFiniteCompact_iff_all_elements_compact` 📖	mathematical	—	`IsSupFiniteCompact` `IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice`	—	`le_refl` `le_sSup` `le_antisymm`
`isSupFiniteCompact_iff_isSupClosedCompact` 📖	mathematical	—	`IsSupFiniteCompact` `IsSupClosedCompact`	—	`List.TFAE.out` `wellFoundedGT_characterisations`
`wellFoundedGT_characterisations` 📖	mathematical	—	`List.TFAE` `WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `IsSupFiniteCompact` `IsSupClosedCompact`	—	`WellFoundedGT.isSupFiniteCompact` `IsSupFiniteCompact.isSupClosedCompact` `IsSupClosedCompact.wellFoundedGT` `isSupFiniteCompact_iff_all_elements_compact` `List.tfae_of_cycle`
`wellFoundedGT_iff_isSupFiniteCompact` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `toConditionallyCompleteLattice` `IsSupFiniteCompact`	—	`List.TFAE.out` `wellFoundedGT_characterisations`

CompleteLattice.IsCompactElement

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`directed_sSup_lt_of_lt` 📖	mathematical	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set.Nonempty` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`CompleteLattice.sSup_le` `LT.lt.le` `eq_iff_le_not_lt` `CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le` `Eq.le` `LT.lt.ne` `LE.le.antisymm`
`exists_finset_of_le_iSup` 📖	mathematical	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLE` `PartialOrder.toPreorder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Finset` `Finset.instMembership`	—	`iSup_le_iSup_of_subset` `Finset.subset_union_left` `Finset.subset_union_right` `LE.le.trans` `iSup_le` `le_sSup_of_le` `le_iSup_of_le` `Finset.mem_singleton_self` `le_rfl` `CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le` `Set.range_nonempty`

CompleteLattice.IsSupClosedCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSupFiniteCompact` 📖	mathematical	`CompleteLattice.IsSupClosedCompact`	`CompleteLattice.IsSupFiniteCompact`	—	`CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact`
`wellFoundedGT` 📖	mathematical	`CompleteLattice.IsSupClosedCompact`	`WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`RelEmbedding.wellFounded_iff_isEmpty` `instIsStrictOrderGt` `Set.mem_range_self` `RelHomClass.map_sup` `RelEmbedding.instRelHomClass` `Set.mem_range` `RelEmbedding.map_rel_iff` `lt_irrefl` `lt_of_le_of_lt` `CompleteLattice.le_sSup`

CompleteLattice.IsSupFiniteCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSupClosedCompact` 📖	mathematical	`CompleteLattice.IsSupFiniteCompact`	`CompleteLattice.IsSupClosedCompact`	—	`Finset.eq_empty_or_nonempty` `Finset.sup_empty` `eq_singleton_bot_of_sSup_eq_bot_of_nonempty` `SupClosed.finsetSup_mem`
`wellFoundedGT` 📖	mathematical	`CompleteLattice.IsSupFiniteCompact`	`WellFoundedGT` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact`

CompleteLattice.WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSupClosedCompact` 📖	mathematical	—	`CompleteLattice.IsSupClosedCompact`	—	`CompleteLattice.isSupClosedCompact_iff_wellFoundedGT`
`isSupFiniteCompact` 📖	mathematical	—	`CompleteLattice.IsSupFiniteCompact`	—	`WellFounded.has_min` `wellFounded_gt` `Finset.coe_empty` `Finset.sup_empty` `LE.le.antisymm` `CompleteLattice.sSup_le` `eq_of_le_of_not_lt` `Finset.sup_mono` `Finset.subset_insert` `Finset.coe_insert` `Finset.sup_insert` `Finset.sup_id_eq_sSup` `sSup_le_sSup`

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_iSup_left` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`iSup_inf_eq`
`disjoint_iSup_right` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`inf_iSup_eq`
`iSup_inf_eq` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`iSup.eq_1` `DirectedOn.sSup_inf_eq` `directedOn_range` `iSup_range`
`inf_iSup_eq` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`iSup.eq_1` `DirectedOn.inf_sSup_eq` `directedOn_range` `iSup_range`

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_sSup_left` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`sSup_inf_eq`
`disjoint_sSup_right` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`inf_sSup_eq`
`inf_sSup_eq` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `iSup` `Set` `Set.instMembership`	—	`le_antisymm` `le_iff_compact_le_imp` `CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le` `le_inf_iff` `LE.le.trans` `le_inf` `le_biSup` `Set.not_nonempty_iff_eq_empty` `sSup_empty` `inf_of_le_right` `iSup_congr_Prop` `iSup_neg` `iSup_bot` `iSup_inf_le_inf_sSup`
`sSup_inf_eq` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `iSup` `Set` `Set.instMembership`	—	`inf_comm` `iSup_congr_Prop` `inf_sSup_eq`

IsCompactlyGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sSup_eq` 📖	mathematical	—	`IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—

WellFoundedGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_ne_bot_of_iSupIndep` 📖	mathematical	`iSupIndep`	`Set.Finite` `setOf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Set.Finite.of_finite_image` `Set.Finite.subset` `finite_of_sSupIndep` `iSupIndep.sSupIndep_range` `Set.image_subset_range` `iSupIndep.injOn`
`finite_of_iSupIndep` 📖	mathematical	`iSupIndep`	`Finite`	—	`Finite.of_injective_finite_range` `iSupIndep.injective` `Set.Finite.to_subtype` `finite_of_sSupIndep` `iSupIndep.sSupIndep_range`
`finite_of_sSupIndep` 📖	mathematical	`sSupIndep`	`Set.Finite`	—	`CompleteLattice.WellFoundedGT.isSupFiniteCompact` `Set.Infinite.diff` `Finset.finite_toSet` `Set.Infinite.nonempty` `Finset.coe_insert` `sSupIndep.mono` `Set.union_singleton` `Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `Finset.sup_id_eq_sSup` `Disjoint.eq_bot` `inf_eq_left` `le_sSup`

WellFoundedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_ne_bot_of_iSupIndep` 📖	mathematical	`iSupIndep`	`Set.Finite` `setOf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Set.Finite.of_finite_image` `Set.Finite.subset` `finite_of_sSupIndep` `iSupIndep.sSupIndep_range` `Set.image_subset_range` `iSupIndep.injOn`
`finite_of_iSupIndep` 📖	mathematical	`iSupIndep`	`Finite`	—	`Finite.of_injective_finite_range` `iSupIndep.injective` `Set.Finite.to_subtype` `finite_of_sSupIndep` `iSupIndep.sSupIndep_range`
`finite_of_sSupIndep` 📖	mathematical	`sSupIndep`	`Set.Finite`	—	`Set.Infinite.to_subtype` `Set.Infinite.diff` `Set.finite_singleton` `sup_le_iff` `le_iSup₂_of_le` `le_rfl` `iSup₂_le` `LE.le.trans` `LT.lt.trans_le` `Disjoint.right_lt_sup_of_left_ne_bot` `Disjoint.mono_right` `le_sSup` `LT.lt.not_ge` `LE.le.trans_eq` `Function.Embedding.inj'` `Subtype.val_injective` `RelEmbedding.not_wellFounded` `instIsStrictOrderLt` `wellFounded_lt`

(root)

Definitions

Name	Category	Theorems
`IsCompactElement` 📖	MathDef	17 math math: `TopologicalSpace.Opens.isCompactElement_iff`, `LieSubmodule.isCompactElement_lieSpan_singleton`, `IntermediateField.adjoin_simple_isCompactElement`, `IntermediateField.adjoin_finite_isCompactElement`, `Submodule.finite_span_isCompactElement`, `sSup_compact_eq_top`, `CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup`, `Submodule.singleton_span_isCompactElement`, `IsCompactlyGenerated.exists_sSup_eq`, `Ideal.isCompactElement_top`, `IntermediateField.adjoin_finset_isCompactElement`, `sSup_compact_le_eq`, `CompleteLattice.isSupFiniteCompact_iff_all_elements_compact`, `Submodule.fg_iff_compact`, `CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup`, `Submodule.finset_span_isCompactElement`, `CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le`
`IsCompactlyGenerated` 📖	CompData	5 math math: `Submodule.instIsCompactlyGenerated`, `CompleteLattice.isCompactlyGenerated_of_wellFoundedGT`, `IntermediateField.instIsCompactlyGenerated`, `LieSubmodule.instIsCompactlyGenerated`, `Set.Iic.instIsCompactlyGenerated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complementedLattice_iff_isAtomistic` 📖	mathematical	—	`ComplementedLattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteLattice.toBoundedOrder` `IsAtomistic` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`isAtomistic_of_complementedLattice` `complementedLattice_of_isAtomistic`
`complementedLattice_of_isAtomistic` 📖	mathematical	—	`ComplementedLattice` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteLattice.toBoundedOrder`	—	`complementedLattice_of_sSup_atoms_eq_top` `sSup_atoms_eq_top`
`complementedLattice_of_sSup_atoms_eq_top` 📖	mathematical	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `IsAtom` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop`	`ComplementedLattice` `ConditionallyCompleteLattice.toLattice`	—	`exists_sSupIndep_isCompl_sSup_atoms`
`exists_sSupIndep_disjoint_sSup_atoms` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `setOf` `IsAtom` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`sSupIndep` `Disjoint` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`zorn_subset` `iSupIndep_sUnion_of_directed` `IsChain.directedOn` `Set.instReflSubset` `sSup_sUnion` `sSup_image` `DirectedOn.disjoint_sSup_right` `directedOn_image` `DirectedOn.mono` `sSup_le_sSup` `Set.subset_sUnion_of_mem` `le_antisymm` `sSup_le_iff` `inf_eq_left` `IsAtom.le_iff` `inf_le_left` `LE.le.trans` `le_sSup` `Disjoint.mono_right` `le_sup_right` `disjoint_iff` `eq_or_ne` `Set.union_singleton` `Set.insert_diff_of_mem` `Set.diff_subset` `Set.mem_singleton_iff` `Set.mem_union` `Set.insert_diff_of_notMem` `sSup_union` `sSup_singleton` `Disjoint.disjoint_sup_right_of_disjoint_sup_left` `Disjoint.symm` `sSup_insert` `Set.insert_diff_singleton` `Set.insert_eq_of_mem` `le_refl` `Set.subset_union_left` `Set.mem_union_right` `Set.mem_singleton`
`exists_sSupIndep_isCompl_sSup_atoms` 📖	mathematical	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `IsAtom` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop`	`sSupIndep` `IsCompl`	—	`exists_sSupIndep_disjoint_sSup_atoms` `le_top`
`exists_sSupIndep_of_sSup_atoms` 📖	mathematical	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `IsAtom` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`sSupIndep`	—	`exists_sSupIndep_disjoint_sSup_atoms` `bot_le` `sup_of_le_right`
`exists_sSupIndep_of_sSup_atoms_eq_top` 📖	mathematical	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `IsAtom` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop`	`sSupIndep`	—	`exists_sSupIndep_of_sSup_atoms`
`iSupIndep_iff_supIndep_of_injOn` 📖	mathematical	`Set.InjOn` `setOf` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`iSupIndep` `Finset.SupIndep` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`iSupIndep.supIndep'` `iSupIndep_def'` `inf_sSup_eq_iSup_inf_sup_finset` `Finset.sup_erase_bot` `Finset.coe_erase` `Finset.ext` `Finset.erase_insert_eq_erase` `Finset.sup_image` `Finset.supIndep_iff_disjoint_erase` `Finset.mem_insert_self`
`iSupIndep_sUnion_of_directed` 📖	mathematical	`DirectedOn` `Set` `Set.instHasSubset` `sSupIndep`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `sSupIndep_iUnion_of_directed` `DirectedOn.directed_val`
`inf_sSup_eq_iSup_inf_sup_finset` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iSup` `Finset` `Set` `Set.instHasSubset` `SetLike.coe` `Finset.instSetLike` `Finset.sup` `Lattice.toSemilatticeSup` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	—	`le_antisymm` `le_iff_compact_le_imp` `CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup` `le_inf_iff` `LE.le.trans` `le_inf` `le_iSup₂` `iSup_le` `inf_le_inf_left` `sSup_le_sSup` `Finset.sup_id_eq_sSup`
`isAtomic_of_complementedLattice` 📖	mathematical	—	`IsAtomic` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`sSup_compact_le_eq` `sSup_eq_bot` `Set.not_subset` `CompleteLattice.Iic_coatomic_of_compact_element` `le_refl` `IsAtomic.eq_bot_or_exists_atom_le` `isAtomic_iff_isCoatomic` `IsModularLattice.isModularLattice_Iic` `IsModularLattice.complementedLattice_Iic` `IsAtom.of_isAtom_coe_Iic` `LE.le.trans` `Subtype.coe_le_coe`
`isAtomistic_of_complementedLattice` 📖	mathematical	—	`IsAtomistic` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder`	—	`CompleteLattice.isAtomistic_iff` `sSup_le` `lt_or_eq_of_le` `ComplementedLattice.exists_isCompl` `IsModularLattice.complementedLattice_Iic` `IsAtomic.eq_bot_or_exists_atom_le` `IsAtomic.Set.Iic.isAtomic` `isAtomic_of_complementedLattice` `ne_of_lt` `eq_top_of_isCompl_bot` `eq_bot_iff` `le_trans` `le_inf` `Subtype.coe_le_coe` `le_sSup` `IsAtom.of_isAtom_coe_Iic` `Disjoint.le_bot` `IsCompl.disjoint`
`le_iff_compact_le_imp` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`le_trans` `sSup_compact_le_eq` `sSup_le_sSup`
`sSupIndep_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `Set.instHasSubset` `sSupIndep`	`Set.iUnion`	—	`sSupIndep_iff_finite` `Set.finite_subset_iUnion` `Finset.finite_toSet` `Directed.finset_le` `Set.instIsTransSubset` `sSupIndep.mono` `Set.Subset.trans` `Set.iUnion₂_subset` `Set.Finite.mem_toFinset`
`sSupIndep_iff_finite` 📖	mathematical	—	`sSupIndep` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`sSupIndep.mono` `disjoint_iff` `inf_sSup_eq_iSup_inf_sup_finset` `iSup_eq_bot` `Finset.sup_id_eq_sSup` `Disjoint.eq_bot` `Finset.coe_insert` `Set.insert_subset_iff` `Set.Subset.trans` `Set.diff_subset` `Finset.mem_insert_self` `Set.insert_diff_self_of_notMem` `Set.mem_diff` `Set.mem_singleton`
`sSup_compact_eq_top` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`sSup_compact_le_eq`
`sSup_compact_le_eq` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `setOf` `IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `Preorder.toLE` `PartialOrder.toPreorder`	—	`IsCompactlyGenerated.exists_sSup_eq` `le_antisymm` `sSup_le` `sSup_le_sSup` `le_sSup`

iSupIndep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf` 📖	mathematical	`iSupIndep`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	—	`iSupIndep_iff_supIndep_of_injOn` `injOn_iInf` `Finset.one_lt_card_iff` `Function.ne_iff` `Finset.image_biUnion_filter_eq` `Finset.SupIndep.biUnion` `Finset.SupIndep.mono` `supIndep'` `iInf_le`

---

← Back to Index