sized_iUnion — Mathlib

English

Let f : ι → Set (Finset α). Then the r-sizedness of the union equals the universal r-sizedness of all fibers: (⋃ i, f i).Sized r ↔ ∀ i, (f i).Sized r.

Русский

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

LaTeX

$$$ (\bigcup_i f_i).Sized r \iff \forall i, (f_i).Sized r $$$

Lean4

@[simp]
theorem sized_iUnion {f : ι → Set (Finset α)} : (⋃ i, f i).Sized r ↔ ∀ i, (f i).Sized r :=
  by
  simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]
  exact forall_swap

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