mk_inf_mk — Mathlib

English

If a,b ∈ α with ha ∈ L and hb ∈ L, then the meet of ⟨a,ha⟩ and ⟨b,hb⟩ in L is ⟨a ⊓ b, L.infClosed ha hb⟩.

Русский

Если a,b ∈ α и ha,hb ∈ L, то произведение ⟨a,ha⟩ и ⟨b,hb⟩ в подрешетке L равно ⟨a ⊓ b, L.infClosed ha hb⟩.

LaTeX

$$$ (\\langle a, ha\\rangle \\downarrow \\langle b, hb\\rangle : L) = \\langle a \\land b, L.infClosed ha hb\\rangle $$$

Lean4

@[simp]
theorem mk_inf_mk (a b : α) (ha hb) : (⟨a, ha⟩ ⊓ ⟨b, hb⟩ : L) = ⟨a ⊓ b, L.infClosed ha hb⟩ :=
  rfl

Похожие утверждения