English
If P is closed under sup and inf, then the natural inclusion map from the sublattice {x∈β | P x} into β is a lattice homomorphism (preserves sup and inf).
Русский
Если P сохраняется под объединением и пересечением, то естественное включение подрешётки {x ∈ β | P x} в β является гомоморфизмом решётки (сохраняет sup и inf).
LaTeX
$$$\text{If } P: \beta \to \text{Prop} \text{ with closed under } \vee \text{ and } \wedge, \text{then }\mathrm{subtypeVal}_{P_s,P_i} : \{x:β \mid P x\} \to β \text{ preserves } \vee \text{ and } \wedge.$$$
Lean4
/-- `Subtype.val` as a `LatticeHom`. -/
def subtypeVal {P : β → Prop} (Psup : ∀ ⦃x y⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y⦄, P x → P y → P (x ⊓ y)) :
letI := Subtype.lattice Psup Pinf
LatticeHom { x : β // P x } β :=
letI := Subtype.lattice Psup Pinf
.mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_inf Pinf])
