English
If a,b ∈ α with ha ∈ L and hb ∈ L, then the join of ⟨a,ha⟩ and ⟨b,hb⟩ in L is ⟨a ⊔ b, L.supClosed ha hb⟩.
Русский
Если a,b ∈ α и ha ∈ L, hb ∈ L, то сумма ⟨a,ha⟩ и ⟨b,hb⟩ в подрешетке L равна ⟨a ⊔ b, L.supClosed ha hb⟩.
LaTeX
$$$ (\\langle a, ha\\rangle \\uparrow \\langle b, hb\\rangle : L) = \\langle a \\uparrow b, L.supClosed ha hb\\rangle $$$
Lean4
@[simp]
theorem mk_sup_mk (a b : α) (ha hb) : (⟨a, ha⟩ ⊔ ⟨b, hb⟩ : L) = ⟨a ⊔ b, L.supClosed ha hb⟩ :=
rfl