u_sup_l — Mathlib

English

Let gi be a Galois Coinsertion; then u(l a ⊔ l b) = a ⊔ b for semilattice sup, and symmetrically in the dual for inf.

Русский

Пусть gi — связь Галуа-коинсерция; тогда u(l a ⊔ l b) = a ⊔ b для верхней границы, а симметрично в двойственности для Inf.

LaTeX

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

Lean4

theorem u_sup_l [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisCoinsertion l u) (a b : α) : u (l a ⊔ l b) = a ⊔ b :=
  gi.dual.l_inf_u _ _

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