Lattice

Statistics

Metric	Count
Definitions	0
Theorems `gc_upperBounds_lowerBounds`, `isGLB_iUnion_iff_of_isLUB`, `isLUB_iUnion_iff_of_isLUB`, `lowerBounds_iUnion`, `upperBounds_iUnion`	5
Total	5

Name	Kind	Assumes	Proves	Validates	Depends On
`gc_upperBounds_lowerBounds` 📖	mathematical	—	`GaloisConnection` `Set` `OrderDual` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `upperBounds` `Preorder.toLE` `lowerBounds` `OrderDual.ofDual`	—	`forall₂_swap`
`isGLB_iUnion_iff_of_isLUB` 📖	mathematical	`IsGLB` `Preorder.toLE`	`Set.range` `Set.iUnion`	—	`isGLB_congr` `Set.range_eq_iUnion` `lowerBounds_iUnion` `lowerBounds_singleton` `IsGLB.lowerBounds_eq`
`isLUB_iUnion_iff_of_isLUB` 📖	mathematical	`IsLUB` `Preorder.toLE`	`Set.range` `Set.iUnion`	—	`isLUB_congr` `Set.range_eq_iUnion` `upperBounds_iUnion` `upperBounds_singleton` `IsLUB.upperBounds_eq`
`lowerBounds_iUnion` 📖	mathematical	—	`lowerBounds` `Preorder.toLE` `Set.iUnion` `Set.iInter`	—	`GaloisConnection.u_iInf` `gc_upperBounds_lowerBounds`
`upperBounds_iUnion` 📖	mathematical	—	`upperBounds` `Preorder.toLE` `Set.iUnion` `Set.iInter`	—	`GaloisConnection.l_iSup` `gc_upperBounds_lowerBounds`

---