u_iSup_l — Mathlib

English

Let gi be a Galois Coinsertion; then u(iSup i (l(f(i)))) = iSup i f(i) for f: ι → α.

Русский

Пусть gi — связка Галуа-коинсерция; тогда u(⊔_i l(f(i))) = ⊔_i f(i) для f: ι → α.

LaTeX

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

Lean4

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

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