English
Let α be a lattice and P : α → Prop with Psup and Pinf preserving ⊔ and ⊓ respectively; then the subtype { x ∈ α | P x } carries a lattice structure, with join and meet defined by the lifted operations.
Русский
Пусть α — решетка и P : α → Prop such that Psup и Pinf сохраняют ⊔ и ⊓ соответственно; тогда подтип { x ∈ α | P x } образует структуру решетки, где операция наибольшего и наименьшего возведены в соответствующий подтип.
LaTeX
$$$[Lattice\\;\\alpha] \\, \\{P:\\alpha\\to\\mathrm{Prop}\\} \\, (Psup:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcup y)) \\, (Pinf:\\forall\\{x\\,y\\}, P x\\to P y\\to P(x\\sqcap y)) \Rightarrow \\mathrm{Lattice}\\left(\\{ x:\\alpha \\mid P x\\} \\right)$$$
Lean4
/-- A subtype forms a lattice if `⊔` and `⊓` preserve the property.
See note [reducible non-instances]. -/
protected abbrev lattice [Lattice α] {P : α → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y))
(Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) : Lattice { x : α // P x }
where
__ := Subtype.semilatticeInf Pinf
__ := Subtype.semilatticeSup Psup
