u_biSup_l — Mathlib

English

If f: ι → β and hf: ∀ i, l(u(f(i))) = f(i), then u( ⨆ i f(i) ) = ⨆ i u(f(i)).

Русский

Если дана функция f: ι → β и hf: ∀ i, l(u(f(i))) = f(i), то u(⊔_i f(i)) = ⊔_i u(f(i)).

LaTeX

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

Lean4

theorem u_biSup_l [CompleteLattice α] [CompleteLattice β] (gi : GaloisCoinsertion l u) {ι : Sort x} {p : ι → Prop}
    (f : ∀ (i) (_ : p i), α) : u (⨆ (i) (hi), l (f i hi)) = ⨆ (i) (hi), f i hi :=
  gi.dual.l_biInf_u _

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