u_iSup_of_lu_eq_self — Mathlib

English

Same as 160711: given hf: ∀ i, l(u(f(i))) = f(i), then u(⊔_i f(i)) = ⊔_i u(f(i)).

Русский

То же, что и 160711: hf обеспечивает равенство.

LaTeX

$$$$ u\left( \bigvee_{i} f(i) \right) = \bigvee_{i} u\big(f(i)\big). $$$$

Lean4

theorem u_iSup_of_lu_eq_self [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x}
    (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) : u (⨆ i, f i) = ⨆ i, u (f i) :=
  gi.dual.l_iInf_of_ul_eq_self _ hf

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