Lattice

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

Statistics

Metric	Count
Definitions `fintypeBiUnion`, `fintypeBiUnion'`, `fintypeiUnion`, `fintypesUnion`	4
Theorems `exists_mem_subset_of_finset_subset_biUnion`, `exists_mem_subset_of_finite_of_subset_sUnion`, `exists_mem_subset_of_finset_subset_biUnion`, `finite_biUnion`, `finite_biUnion'`, `finite_biUnion''`, `finite_iInter`, `finite_iUnion`, `finite_sUnion`, `bddAbove`, `bddBelow`, `bddAbove`, `bddAbove_biUnion`, `bddBelow`, `bddBelow_biUnion`, `biUnion`, `biUnion'`, `iInf_biSup_of_antitone`, `iInf_biSup_of_monotone`, `iSup_biInf_of_antitone`, `iSup_biInf_of_monotone`, `iUnion`, `of_finite_fibers`, `preimage'`, `sInter`, `sUnion`, `biUnion`, `iUnion`, `iUnion₂`, `sUnion`, `finite_biUnion_iff`, `eq_finite_iUnion_of_finite_subset_iUnion`, `finite_diff_iUnion_Ioo`, `finite_diff_iUnion_Ioo'`, `finite_iUnion`, `finite_iUnion_iff`, `finite_iUnion_of_subsingleton`, `finite_subset_iUnion`, `iInf_iSup_of_antitone`, `iInf_iSup_of_monotone`, `iInter_iUnion_of_antitone`, `iInter_iUnion_of_monotone`, `iSup_iInf_of_antitone`, `iSup_iInf_of_monotone`, `iUnion_iInter_of_antitone`, `iUnion_iInter_of_monotone`, `iUnion_pi_of_monotone`, `iUnion_univ_pi_of_monotone`, `infinite_iUnion`, `infinite_of_not_bddAbove`, `infinite_of_not_bddBelow`, `map_finite_biInf`, `map_finite_biSup`, `map_finite_iInf`, `map_finite_iSup`, `toFinset_iUnion`, `union_finset_finite_of_range_finite`, `iInf_iSup_of_antitone`, `iInf_iSup_of_monotone`, `iSup_iInf_of_antitone`, `iSup_iInf_of_monotone`	61
Total	65

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_subset_of_finset_subset_biUnion` 📖	—	`Directed` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.iUnion`	—	—	`Finset.cons_induction` `Finset.coe_empty` `Finset.coe_cons` `HasSubset.Subset.trans` `Set.instIsTransSubset`

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_subset_of_finite_of_subset_sUnion` 📖	mathematical	`Set.Nonempty` `Set` `DirectedOn` `Set.instHasSubset` `Set.sUnion`	`Set.instMembership`	—	`exists_mem_subset_of_finset_subset_biUnion` `Set.sUnion_eq_biUnion` `Set.Finite.coe_toFinset`
`exists_mem_subset_of_finset_subset_biUnion` 📖	—	`Set.Nonempty` `DirectedOn` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Set.iUnion` `Set.instMembership`	—	—	`Directed.exists_mem_subset_of_finset_subset_biUnion` `Set.Nonempty.coe_sort` `directed_comp` `directed_val` `Set.biUnion_eq_iUnion`

Finite.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_biUnion` 📖	mathematical	`Finite` `Set.Elem`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `finite_iUnion`
`finite_biUnion'` 📖	mathematical	`Finite` `Set.Elem`	`Set.iUnion` `Set` `Set.instMembership`	—	`finite_biUnion`
`finite_biUnion''` 📖	mathematical	`Finite` `Set.Elem`	`Set.iUnion`	—	`finite_biUnion'`
`finite_iInter` 📖	mathematical	`Finite` `Set.Elem`	`Set.iInter`	—	`subset` `Set.iInter_subset`
`finite_iUnion` 📖	mathematical	`Finite` `Set.Elem`	`Set.iUnion`	—	`instFinitePLift` `Fintype.finite`
`finite_sUnion` 📖	mathematical	`Finite` `Set.Elem` `Set` `Set.instMembership`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `finite_iUnion`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.coe` `Finset` `instSetLike`	—	`Set.Finite.bddAbove` `SemilatticeSup.instIsDirectedOrder` `finite_toSet`
`bddBelow` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.coe` `Finset` `instSetLike`	—	`Set.Finite.bddBelow` `SemilatticeInf.instIsCodirectedOrder` `finite_toSet`

Set

Definitions

Name	Category	Theorems
`fintypeBiUnion` 📖	CompOp	—
`fintypeBiUnion'` 📖	CompOp	—
`fintypeiUnion` 📖	CompOp	1 math math: `toFinset_iUnion`
`fintypesUnion` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_finite_iUnion_of_finite_subset_iUnion` 📖	mathematical	`Set` `instHasSubset` `iUnion`	`Finite` `instMembership` `setOf` `Elem`	—	`finite_subset_iUnion` `Finite.subset` `inter_subset_right` `inter_subset_left` `ext` `mem_iUnion`
`finite_diff_iUnion_Ioo` 📖	mathematical	—	`Finite` `Set` `instSDiff` `iUnion` `instMembership` `Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`finite_of_forall_not_lt_lt` `mem_iUnion₂_of_mem`
`finite_diff_iUnion_Ioo'` 📖	mathematical	—	`Finite` `Set` `instSDiff` `iUnion` `Elem` `Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instMembership`	—	`iSup_prod` `iSup_subtype` `iSup_congr_Prop` `finite_diff_iUnion_Ioo`
`finite_iUnion` 📖	mathematical	`Finite`	`iUnion`	—	`toFinite` `Finite.Set.finite_iUnion` `Finite.to_subtype`
`finite_iUnion_iff` 📖	mathematical	`Pairwise` `Disjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Finite` `iUnion` `setOf` `Nonempty`	—	`Finite.subset` `subset_iUnion` `mem_iUnion` `Pairwise.eq` `not_disjoint_iff` `Finite.of_injective` `Finite.iUnion`
`finite_iUnion_of_subsingleton` 📖	mathematical	—	`Finite` `iUnion`	—	`iUnion_plift_down` `finite_iUnion_iff` `Subsingleton.pairwise`
`finite_subset_iUnion` 📖	mathematical	`Set` `instHasSubset` `iUnion`	`Finite` `instMembership`	—	`Finite.to_subtype` `finite_range` `biUnion_range` `mem_iUnion`
`iInf_iSup_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iInf_iSup_of_antitone`
`iInf_iSup_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iInf_iSup_of_monotone`
`iInter_iUnion_of_antitone` 📖	mathematical	`Antitone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iInter` `iUnion`	—	`iInf_iSup_of_antitone`
`iInter_iUnion_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iInter` `iUnion`	—	`iInf_iSup_of_monotone`
`iSup_iInf_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`iSup_iInf_of_antitone`
`iSup_iInf_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`iSup_iInf_of_monotone`
`iUnion_iInter_of_antitone` 📖	mathematical	`Antitone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iUnion` `iInter`	—	`iSup_iInf_of_antitone`
`iUnion_iInter_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iUnion` `iInter`	—	`iSup_iInf_of_monotone`
`iUnion_pi_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iUnion` `pi`	—	`pi_def` `biInter_eq_iInter` `iInter_congr_Prop` `preimage_iUnion` `iUnion_iInter_of_monotone` `Fintype.finite` `SemilatticeSup.instIsDirectedOrder` `preimage_mono`
`iUnion_univ_pi_of_monotone` 📖	mathematical	`Monotone` `Set` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	`iUnion` `pi` `univ`	—	`iUnion_pi_of_monotone` `finite_univ`
`infinite_iUnion` 📖	mathematical	`Set`	`Infinite` `iUnion`	—	`not_injective_infinite_finite` `Finite.to_subtype` `Finite.finite_subsets` `subset_iUnion`
`infinite_of_not_bddAbove` 📖	mathematical	`BddAbove` `Preorder.toLE`	`Infinite`	—	`Finite.bddAbove`
`infinite_of_not_bddBelow` 📖	mathematical	`BddBelow` `Preorder.toLE`	`Infinite`	—	`Finite.bddBelow`
`map_finite_biInf` 📖	mathematical	—	`DFunLike.coe` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `instMembership`	—	`map_finset_inf` `Finset.inf_eq_iInf` `iInf_congr_Prop` `Finite.mem_toFinset`
`map_finite_biSup` 📖	mathematical	—	`DFunLike.coe` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `instMembership`	—	`map_finset_sup` `Finset.sup_eq_iSup` `iSup_congr_Prop` `Finite.mem_toFinset`
`map_finite_iInf` 📖	mathematical	—	`DFunLike.coe` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iInf_univ` `map_finite_biInf` `finite_univ`
`map_finite_iSup` 📖	mathematical	—	`DFunLike.coe` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_univ` `map_finite_biSup` `finite_univ`
`toFinset_iUnion` 📖	mathematical	—	`toFinset` `iUnion` `fintypeiUnion` `PLift.fintype` `Finset.biUnion` `Finset.univ`	—	`Finset.ext`
`union_finset_finite_of_range_finite` 📖	mathematical	—	`Finite` `iUnion` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`biUnion_range` `Finite.biUnion` `Finset.finite_toSet`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove` 📖	mathematical	—	`BddAbove` `Preorder.toLE`	—	`induction_on` `bddAbove_empty` `BddAbove.insert`
`bddAbove_biUnion` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.iUnion` `Set` `Set.instMembership`	—	`induction_on` `Set.biUnion_empty` `Set.biUnion_insert`
`bddBelow` 📖	mathematical	—	`BddBelow` `Preorder.toLE`	—	`bddAbove` `OrderDual.isDirected_le` `OrderDual.instNonempty`
`bddBelow_biUnion` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.iUnion` `Set` `Set.instMembership`	—	`bddAbove_biUnion` `OrderDual.isDirected_le` `OrderDual.instNonempty`
`biUnion` 📖	mathematical	`Set.Finite`	`Set.iUnion` `Set` `Set.instMembership`	—	`biUnion'`
`biUnion'` 📖	mathematical	`Set.Finite`	`Set.iUnion` `Set` `Set.instMembership`	—	`to_subtype` `Set.biUnion_eq_iUnion` `Set.finite_iUnion`
`iInf_biSup_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	—	`iSup_biInf_of_monotone` `Antitone.dual_right`
`iInf_biSup_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	—	`iSup_biInf_of_antitone` `Monotone.dual_right`
`iSup_biInf_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet` `Set` `Set.instMembership`	—	`iSup_biInf_of_monotone` `OrderDual.instNonempty` `OrderDual.isDirected_le` `Antitone.dual_left`
`iSup_biInf_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet` `Set` `Set.instMembership`	—	`induction_on` `iInf_congr_Prop` `iInf_neg` `iInf_top` `iSup_const` `iInf_insert` `Set.forall_mem_insert` `iSup_inf_of_monotone` `iInf₂_mono`
`iUnion` 📖	mathematical	`Set.Finite` `Set` `Set.instEmptyCollection`	`Set.iUnion`	—	`Set.iUnion_subset` `Set.mem_biUnion` `Set.mem_empty_iff_false` `subset` `biUnion`
`of_finite_fibers` 📖	—	`Set.Finite` `Set` `Set.instInter` `Set.preimage` `Set.instSingletonSet`	—	—	`subset` `biUnion` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right`
`preimage'` 📖	—	`Set.Finite` `Set.preimage` `Set` `Set.instSingletonSet`	—	—	`Set.biUnion_preimage_singleton` `biUnion`
`sInter` 📖	mathematical	`Set` `Set.instMembership`	`Set.Finite` `Set.sInter`	—	`subset` `Set.sInter_subset_of_mem`
`sUnion` 📖	mathematical	`Set.Finite`	`Set.sUnion`	—	`Set.sUnion_eq_biUnion` `biUnion`

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion` 📖	mathematical	`Set.Infinite` `Set.InjOn` `Set`	`Set.iUnion` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `to_subtype` `Set.infinite_iUnion`
`iUnion` 📖	mathematical	`Set.Infinite`	`Set.iUnion`	—	`Set.Finite.subset` `Set.subset_iUnion`
`iUnion₂` 📖	mathematical	`Set.Infinite`	`Set.iUnion`	—	`Set.Finite.subset` `Set.subset_iUnion₂`
`sUnion` 📖	mathematical	`Set.Infinite` `Set`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `to_subtype` `Set.infinite_iUnion` `Subtype.coe_injective`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_biUnion_iff` 📖	mathematical	`Set.PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Set.Finite` `Set.iUnion` `Set.instMembership` `setOf` `Set.Nonempty`	—	`Set.finite_iUnion_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_iSup_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_iInf_of_monotone` `Antitone.dual_right`
`iInf_iSup_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Coframe.toCompleteLattice`	`iInf` `CompleteSemilatticeInf.toInfSet` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_iInf_of_antitone` `Monotone.dual_right`
`iSup_iInf_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`iSup_iInf_of_monotone` `OrderDual.instNonempty` `OrderDual.isDirected_le` `Antitone.dual_left`
`iSup_iInf_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Order.Frame.toCompleteLattice`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`iInf_univ` `Set.Finite.iSup_biInf_of_monotone` `Set.finite_univ`

---

← Back to Index