sized_iUnion₂ — Mathlib

English

Let f : ∀ i, κ i → Set (Finset α). The r-sizedness of the double-index union is equivalent to each fiber being r-sized: (⋃ i, ⋃ j, f i j).Sized r ↔ ∀ i j, (f i j).Sized r.

Русский

Пусть f : ∀ i, κ i → Set(Finset α). r-размерность объединения по двум индексам равна размерности во всех элементах: (⋃ i, ⋃ j, f i j).Sized r ⇔ ∀ i j, (f i j).Sized r.

LaTeX

$$$ (\bigcup_i \bigcup_j f_{i j}).Sized r \iff \forall i,\forall j, (f_{i j}).Sized r $$$

Lean4

theorem sized_iUnion₂ {f : ∀ i, κ i → Set (Finset α)} : (⋃ (i) (j), f i j).Sized r ↔ ∀ i j, (f i j).Sized r := by
  simp only [Set.sized_iUnion]

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