Lemmas

📁 Source: Mathlib/Order/CompleteLattice/Lemmas.lean

Statistics

Metric	Count
Definitions `instCompleteLinearOrder`, `infSet`, `instCompleteLattice`, `supSet`	4
Theorems `iInf_nat_add`, `iSup_nat_add`, `down_iInf`, `down_iSup`, `down_sInf`, `down_sSup`, `up_iInf`, `up_iSup`, `up_sInf`, `up_sSup`, `biInf_sup_le_biInf_sup`, `biSup_inf_le_biSup_inf`, `biSup_inf_le_inf_biSup`, `disjoint_of_sSup_disjoint`, `disjoint_of_sSup_disjoint_of_le_of_le`, `disjoint_sSup_left`, `disjoint_sSup_right`, `iInf_bool_eq`, `iInf_ge_eq_iInf_nat_add`, `iInf_iSup_ge_nat_add`, `iInf_nat_gt_zero_eq`, `iInf_sup_iInf_le`, `iInf_sup_le_iInf_sup`, `iSup_bool_eq`, `iSup_ge_eq_iSup_nat_add`, `iSup_iInf_ge_nat_add`, `iSup_inf_le_iSup_inf`, `iSup_inf_le_inf_iSup`, `iSup_inf_le_inf_sSup`, `iSup_inf_le_sSup_inf`, `iSup_nat_gt_zero_eq`, `inf_eq_iInf`, `inf_iInf_nat_succ`, `le_iSup_inf_iSup`, `sInf_sup_le_iInf_sup`, `sup_biInf_le_biInf_sup`, `sup_eq_iSup`, `sup_iInf_le_iInf_sup`, `sup_iSup_nat_succ`, `sup_sInf_le_iInf_sup`	40
Total	44

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_nat_add` 📖	mathematical	`Antitone` `Nat.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iInf` `CompleteSemilatticeInf.toInfSet`	—	`Monotone.iSup_nat_add` `dual_right`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_nat_add` 📖	mathematical	`Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`le_antisymm` `iSup_le` `le_iSup` `iSup_mono`

PUnit

Definitions

Name	Category	Theorems
`instCompleteLinearOrder` 📖	CompOp	—

ULift

Definitions

Name	Category	Theorems
`infSet` 📖	CompOp	4 math math: `up_sInf`, `down_iInf`, `down_sInf`, `up_iInf`
`instCompleteLattice` 📖	CompOp	—
`supSet` 📖	CompOp	4 math math: `down_sSup`, `up_sSup`, `up_iSup`, `down_iSup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`down_iInf` 📖	mathematical	—	`iInf` `infSet`	—	`Set.preimage_eq_iff_eq_image` `up_bijective` `Set.range_comp`
`down_iSup` 📖	mathematical	—	`iSup` `supSet`	—	`Set.preimage_eq_iff_eq_image` `up_bijective` `Set.range_comp`
`down_sInf` 📖	mathematical	—	`InfSet.sInf` `infSet` `Set.preimage`	—	—
`down_sSup` 📖	mathematical	—	`SupSet.sSup` `supSet` `Set.preimage`	—	—
`up_iInf` 📖	mathematical	—	`iInf` `infSet`	—	`down_iInf`
`up_iSup` 📖	mathematical	—	`iSup` `supSet`	—	`down_iSup`
`up_sInf` 📖	mathematical	—	`InfSet.sInf` `infSet` `Set.preimage`	—	—
`up_sSup` 📖	mathematical	—	`SupSet.sSup` `supSet` `Set.preimage`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biInf_sup_le_biInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet` `Set` `Set.instMembership`	—	`le_iInf₂` `sup_le_sup_right` `biInf_le`
`biSup_inf_le_biSup_inf` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`biInf_sup_le_biInf_sup`
`biSup_inf_le_inf_biSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`sup_biInf_le_biInf_sup`
`disjoint_of_sSup_disjoint` 📖	mathematical	`Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	`SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	—	`disjoint_of_sSup_disjoint_of_le_of_le` `le_sSup`
`disjoint_of_sSup_disjoint_of_le_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	`SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	—	—
`disjoint_sSup_left` 📖	—	`Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	—	—	`disjoint_iff_inf_le` `iSup₂_le_iff` `LE.le.trans` `iSup_inf_le_sSup_inf` `Disjoint.le_bot`
`disjoint_sSup_right` 📖	—	`Disjoint` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership`	—	—	`disjoint_iff_inf_le` `iSup₂_le_iff` `LE.le.trans` `iSup_inf_le_inf_sSup` `Disjoint.le_bot`
`iInf_bool_eq` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`iSup_bool_eq`
`iInf_ge_eq_iInf_nat_add` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iSup_ge_eq_iSup_nat_add`
`iInf_iSup_ge_nat_add` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_iInf_ge_nat_add`
`iInf_nat_gt_zero_eq` 📖	mathematical	—	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`iInf_range` `Nat.range_succ` `iInf_congr_Prop`
`iInf_sup_iInf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`le_iSup_inf_iSup`
`iInf_sup_le_iInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`le_iInf` `sup_le_sup_right` `iInf_le`
`iSup_bool_eq` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice`	—	`iSup.eq_1` `Bool.range_eq` `sSup_pair` `sup_comm`
`iSup_ge_eq_iSup_nat_add` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`le_antisymm` `le_sSup` `iSup_pos`
`iSup_iInf_ge_nat_add` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`biInf_mono` `LE.le.trans` `Monotone.iSup_nat_add` `iInf_ge_eq_iInf_nat_add`
`iSup_inf_le_iSup_inf` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`iInf_sup_le_iInf_sup`
`iSup_inf_le_inf_iSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`sup_iInf_le_iInf_sup`
`iSup_inf_le_inf_sSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `SupSet.sSup`	—	`sup_sInf_le_iInf_sup`
`iSup_inf_le_sSup_inf` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set` `Set.instMembership` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `SupSet.sSup`	—	`sInf_sup_le_iInf_sup`
`iSup_nat_gt_zero_eq` 📖	mathematical	—	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iInf_nat_gt_zero_eq`
`inf_eq_iInf` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`sup_eq_iSup`
`inf_iInf_nat_succ` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf`	—	`sup_iSup_nat_succ`
`le_iSup_inf_iSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`le_inf` `iSup_mono` `inf_le_left` `inf_le_right`
`sInf_sup_le_iInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `iInf` `Set` `Set.instMembership`	—	`le_iInf₂` `sup_le_sup_right` `sInf_le`
`sup_biInf_le_biInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet` `Set` `Set.instMembership`	—	`le_iInf₂` `sup_le_sup_left` `biInf_le`
`sup_eq_iSup` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_bool_eq`
`sup_iInf_le_iInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iInf` `CompleteSemilatticeInf.toInfSet`	—	`le_iInf` `sup_le_sup_left` `iInf_le`
`sup_iSup_nat_succ` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	`iSup_union` `iSup_singleton` `iSup_range` `Nat.zero_union_range_succ` `iSup_univ`
`sup_sInf_le_iInf_sup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `iInf` `Set` `Set.instMembership`	—	`le_iInf₂` `sup_le_sup_left` `sInf_le`

---

← Back to Index