map_iSup₂ — Mathlib

English

A family of arities preserves double-suprema: f(∨_i ∨_j g(i,j)) = ∨_i ∨_j f(g(i,j)).

Русский

Семейство по двум индексам сохраняет двойной наибольший предел: f(∨_i ∨_j g(i,j)) = ∨_i ∨_j f(g(i,j)).

LaTeX

$$$ f\\left( \\big\\vee_i \\big\\vee_j g(i,j) \\right) = \\big\\vee_i \\big\\vee_j f(g(i,j)) $$$

Lean4

theorem map_iSup₂ [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨆ (i) (j), g i j) = ⨆ (i) (j), f (g i j) := by simp_rw [map_iSup]

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