Documentation Verification Report

Lattice

📁 Source: Mathlib/Data/Set/Pairwise/Lattice.lean

Statistics

Metric	Count
Definitions `biUnionEqSigmaOfDisjoint`	1
Theorems `biUnion_injective`, `subset_of_biUnion_subset_biUnion`, `biUnion`, `prod_left`, `subset_of_biUnion_subset_biUnion`, `biUnion_diff_biUnion_eq`, `coe_biUnionEqSigmaOfDisjoint_symm_apply`, `coe_snd_biUnionEqSigmaOfDisjoint`, `pairwiseDisjoint_iUnion`, `pairwiseDisjoint_iff`, `pairwiseDisjoint_pair_insert`, `pairwiseDisjoint_prod_left`, `pairwiseDisjoint_sUnion`, `pairwise_iUnion`, `pairwise_iUnion₂`, `pairwise_iUnion₂_iff`, `pairwise_sUnion`, `pairwiseDisjoint_unique`	18
Total	19

Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_injective` 📖	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.Nonempty`	`Set.iUnion` `Set.instMembership`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `subset_of_biUnion_subset_biUnion` `Eq.subset` `Set.instReflSubset` `Eq.superset`
`subset_of_biUnion_subset_biUnion` 📖	—	`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.Nonempty` `Set.instHasSubset` `Set.iUnion` `Set.instMembership`	—	—	`Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion` `set_pairwise`

Set

Definitions

Name	Category	Theorems
`biUnionEqSigmaOfDisjoint` 📖	CompOp	2 math math: `coe_biUnionEqSigmaOfDisjoint_symm_apply`, `coe_snd_biUnionEqSigmaOfDisjoint`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_diff_biUnion_eq` 📖	mathematical	`PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `instUnion`	`instSDiff` `iUnion` `instMembership`	—	`HasSubset.Subset.antisymm` `instAntisymmSubset` `biUnion_diff_biUnion_subset` `iUnion₂_subset` `mem_diff` `mem_biUnion` `mem_iUnion₂` `Disjoint.le_bot`
`coe_biUnionEqSigmaOfDisjoint_symm_apply` 📖	mathematical	`PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`instMembership` `iUnion` `DFunLike.coe` `Equiv` `Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `biUnionEqSigmaOfDisjoint`	—	—
`coe_snd_biUnionEqSigmaOfDisjoint` 📖	mathematical	`PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`instMembership` `Elem` `DFunLike.coe` `Equiv` `iUnion` `EquivLike.toFunLike` `Equiv.instEquivLike` `biUnionEqSigmaOfDisjoint`	—	`coe_snd_unionEqSigmaOfDisjoint`
`pairwiseDisjoint_iUnion` 📖	mathematical	`Directed` `Set` `instHasSubset`	`PairwiseDisjoint` `iUnion`	—	`pairwise_iUnion`
`pairwiseDisjoint_iff` 📖	mathematical	—	`PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`not_imp_comm`
`pairwiseDisjoint_pair_insert` 📖	mathematical	`Set` `instMembership`	`PairwiseDisjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `powerset` `instInsert` `instSingletonSet`	—	`pairwiseDisjoint_iff` `LeftInvOn.injOn` `insert_erase_invOn` `notMem_subset` `insert_eq_of_mem`
`pairwiseDisjoint_prod_left` 📖	mathematical	—	`PairwiseDisjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `SProd.sprod` `Set` `instSProd` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instMembership`	—	`mk_mem_prod` `PairwiseDisjoint.prod_left`
`pairwiseDisjoint_sUnion` 📖	mathematical	`DirectedOn` `Set` `instHasSubset`	`PairwiseDisjoint` `sUnion`	—	`pairwise_sUnion`
`pairwise_iUnion` 📖	mathematical	`Directed` `Set` `instHasSubset`	`Pairwise` `iUnion`	—	`Pairwise.mono` `subset_iUnion` `mem_iUnion`
`pairwise_iUnion₂` 📖	mathematical	`DirectedOn` `Set` `instHasSubset` `Pairwise`	`iUnion` `instMembership`	—	—
`pairwise_iUnion₂_iff` 📖	mathematical	`DirectedOn` `Set` `instHasSubset`	`Pairwise` `iUnion` `instMembership`	—	`Pairwise.mono` `subset_iUnion₂_of_subset` `subset_refl` `instReflSubset` `pairwise_iUnion₂`
`pairwise_sUnion` 📖	mathematical	`DirectedOn` `Set` `instHasSubset`	`Pairwise` `sUnion`	—	`sUnion_eq_iUnion` `pairwise_iUnion` `DirectedOn.directed_val` `SetCoe.forall`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion` 📖	mathematical	`Set.PairwiseDisjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	`Set.iUnion`	—	`eq_or_ne` `Disjoint.mono` `le_iSup₂`
`prod_left` 📖	mathematical	`Set.PairwiseDisjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	`SProd.sprod` `Set.instSProd`	—	`eq_or_ne` `Disjoint.mono` `le_iSup₂` `Set.mem_prod` `Prod.mk_right_injective`
`subset_of_biUnion_subset_biUnion` 📖	—	`Set.PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instUnion` `Set.Nonempty` `Set.instHasSubset` `Set.iUnion` `Set.instMembership`	—	—	`Set.mem_iUnion₂` `Set.mem_iUnion₂_of_mem` `Set.Pairwise.eq` `Set.subset_union_left` `Set.subset_union_right` `Set.not_disjoint_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwiseDisjoint_unique` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instMembership` `Set.iUnion`	`ExistsUnique`	—	`existsUnique_of_exists_of_unique` `Set.PairwiseDisjoint.elim` `Set.not_disjoint_iff`

---

← Back to Index