l_iSup — Mathlib

English

If l,g forms a Galois connection, then l(iSup_i (iSup_j f(i,j))) = iSup_i (iSup_j f(i,j)).

Русский

Если существует Галуа связь между l и u, то l( sup_i sup_j f(i,j) ) = sup_i sup_j l(f(i,j)).

LaTeX

$$$$ l\\left( \\iint f(i,j) \\right) = \\iint l(f(i,j)) $$$$

Lean4

theorem l_iSup (gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ i, l (f i) :=
  Eq.symm <|
    IsLUB.iSup_eq <|
      show IsLUB (range (l ∘ f)) (l (iSup f)) by rw [range_comp, ← sSup_range]; exact gc.isLUB_l_image (isLUB_sSup _)

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