closure_iUnion₂_closure — Mathlib

English

For f: ∀ i, κ i → α, l(⋃ i (⋃ j, l(f i j))) = l(⋃ i (⋃ j, f i j)).

Русский

Для всякой функции f: ∀ i, κ(i) → α выполняется l(⋃_i⋃_j l(f(i,j))) = l(⋃_i⋃_j f(i,j)).

LaTeX

$$$l\Big(\bigcup_{i} \bigcup_{j} l(f(i,j))\Big) = l\Big(\bigcup_{i} \bigcup_{j} f(i,j)\Big)$$

Lean4

@[simp]
theorem closure_iUnion₂_closure (f : ∀ i, κ i → α) : l (⋃ (i) (j), l (f i j)) = l (⋃ (i) (j), f i j) :=
  SetLike.coe_injective <| l.closure_iSup₂_closure _

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