l_sup — Mathlib

English

For any a₁,a₂ in α, l(a₁ ∨ a₂) = l(a₁) ∨ l(a₂) when (l,u) form a Galois connection.

Русский

Для любых a₁,a₂ ∈ α, при образовании Galois связи l,u выполняется l(a₁ ∨ a₂) = l(a₁) ∨ l(a₂).

LaTeX

$$$$ l(a_1 \\vee a_2) = l a_1 \\vee l a_2 $$$$

Lean4

theorem l_sup (gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂ :=
  (gc.isLUB_l_image isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]

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