mk_inf_mk — Mathlib

English

The meet of two complemented elements is given by the pair ⟨a ⊓ b, ha.inf hb⟩ when a = ⟨a,ha⟩ and b = ⟨b,hb⟩.

Русский

Пересечение двух дополненных элементов определяется как ⟨a ⊓ b, ha.inf hb⟩.

LaTeX

$$$\forall a,b\in \mathrm{Complementeds}(\alpha)\ (ha, hb): IsComplemented(a), IsComplemented(b),\ (⟨a,ha⟩ \land ⟨b,hb⟩) = ⟨a \land b, ha.inf hb⟩$$$

Lean4

@[simp]
theorem mk_inf_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
    (⟨a, ha⟩ ⊓ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊓ b, ha.inf hb⟩ :=
  rfl

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