Lattice

Statistics

Metric	Count
Definitions	0
Theorems `iSup_decode₂`, `iUnion_decode₂`, `iUnion_decode₂_cases`, `iUnion_decode₂_disjoint_on`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_decode₂` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `decode₂`	—	`iSup_comm` `iSup_congr_Prop` `iSup_iSup_eq_right`
`iUnion_decode₂` 📖	mathematical	—	`Set.iUnion` `decode₂`	—	`iSup_decode₂`
`iUnion_decode₂_cases` 📖	mathematical	`Set` `Set.instEmptyCollection`	`Set.iUnion` `decode₂`	—	`Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Set.iUnion_iUnion_eq_right`
`iUnion_decode₂_disjoint_on` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Set.iUnion` `decode₂`	—	`Set.disjoint_left` `Disjoint.le_bot` `Set.iUnion_congr_Prop`

---