Documentation Verification Report

BooleanGenerators

📁 Source: Mathlib/Order/BooleanGenerators.lean

Statistics

Metric	Count
Definitions `BooleanGenerators`, `booleanAlgebra_of_sSup_eq_top`, `distribLattice_of_sSup_eq_top`	3
Theorems `atomistic`, `complementedLattice_of_sSup_eq_top`, `eq_atoms_of_sSup_eq_top`, `finitelyAtomistic`, `isAtom`, `isAtomistic_of_sSup_eq_top`, `mem_of_isAtom_of_le_sSup_atoms`, `mono`, `sSup_inter`, `sSup_le_sSup_iff_of_atoms`	10
Total	13

IsCompactlyGenerated

Definitions

Name	Category	Theorems
`BooleanGenerators` 📖	CompData	1 math math: `LieAlgebra.IsSemisimple.booleanGenerators`

IsCompactlyGenerated.BooleanGenerators

Definitions

Name	Category	Theorems
`booleanAlgebra_of_sSup_eq_top` 📖	CompOp	—
`distribLattice_of_sSup_eq_top` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`atomistic` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Set` `Set.instHasSubset`	—	`IsCompactlyGenerated.exists_sSup_eq` `CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup` `finitelyAtomistic` `Set.Subset.trans` `Finset.sup_id_eq_sSup` `sSup_le` `le_antisymm` `LE.le.trans` `le_sSup` `sSup_le_sSup`
`complementedLattice_of_sSup_eq_top` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`ComplementedLattice` `ConditionallyCompleteLattice.toLattice`	—	`isAtomistic_of_sSup_eq_top` `complementedLattice_of_isAtomistic` `DistribLattice.instIsModularLattice`
`eq_atoms_of_sSup_eq_top` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`setOf` `IsAtom` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BoundedOrder.toOrderBot`	—	`le_antisymm` `isAtom` `atomistic` `LE.le.trans` `le_top` `Eq.ge` `mem_of_isAtom_of_le_sSup_atoms` `sSup_le_sSup`
`finitelyAtomistic` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `IsCompactElement` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `BoundedOrder.toOrderBot` `SemilatticeSup.toPartialOrder` `CompleteLattice.toBoundedOrder`	`Finset.instHasSubset`	—	—
`isAtom` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `Set` `Set.instMembership`	`IsAtom` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder`	—	—
`isAtomistic_of_sSup_eq_top` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`IsAtomistic` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BoundedOrder.toOrderBot`	—	`CompleteLattice.isAtomistic_iff` `atomistic` `le_top` `isAtom`
`mem_of_isAtom_of_le_sSup_atoms` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `IsAtom` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	`Set` `Set.instMembership`	—	`atomistic` `Set.eq_empty_or_nonempty` `sSup_empty` `le_sSup` `IsAtom.le_iff_eq` `isAtom`
`mono` 📖	—	`IsCompactlyGenerated.BooleanGenerators` `Set` `Set.instHasSubset`	—	—	`isAtom` `finitelyAtomistic` `le_trans`
`sSup_inter` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `Set` `Set.instHasSubset`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set.instInter` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice`	—	`le_antisymm` `le_inf` `sSup_le_sSup` `Set.inter_subset_left` `Set.inter_subset_right` `atomistic` `LE.le.trans` `inf_le_left` `sSup_le` `le_sSup` `mem_of_isAtom_of_le_sSup_atoms` `mono` `isAtom` `Eq.ge` `inf_le_right`
`sSup_le_sSup_iff_of_atoms` 📖	mathematical	`IsCompactlyGenerated.BooleanGenerators` `Set` `Set.instHasSubset`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`mem_of_isAtom_of_le_sSup_atoms` `mono` `isAtom` `LE.le.trans` `le_sSup` `sSup_le_sSup`

---

← Back to Index