l_inf_u — Mathlib

English

Let α and β be semilattices with infima and suppose l ⊣ u is a Galois insertion. Then for any a,b in β, l(u(a) ∧ u(b)) = a ∧ b.

Русский

Пусть α, β — полужеподержки с операцией inf, и имеется Галуа-вставка l ⊣ u. Тогда для любых a,b в β выполняется l(u(a) ∧ u(b)) = a ∧ b.

LaTeX

$$$$ l\big(u(a) \wedge u(b)\big) = a \wedge b. $$$$

Lean4

theorem l_inf_u [SemilatticeInf α] [SemilatticeInf β] (gi : GaloisInsertion l u) (a b : β) : l (u a ⊓ u b) = a ⊓ b :=
  calc
    l (u a ⊓ u b) = l (u (a ⊓ b)) := congr_arg l gi.gc.u_inf.symm
    _ = a ⊓ b := by simp only [gi.l_u_eq]

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