squareCylinders_eq_iUnion_image — Mathlib

English

The square cylinders can be expressed as a union of images of certain coordinate maps over all finite index sets.

Русский

Квадратные цилиндры эквивалентны объединению образов некоторых координатных отображений по всем конечным наборам индексов.

LaTeX

$$$$\\text{squareCylinders}(C) = \\bigcup_{s \\in \\mathrm{Finset}\\,\\iota} (\\mathrm{to} \\,s)'' (\\mathrm{univ} \\pi C).$$$$

Lean4

theorem squareCylinders_eq_iUnion_image (C : ∀ i, Set (Set (α i))) :
    squareCylinders C = ⋃ s : Finset ι, (fun t ↦ (s : Set ι).pi t) '' univ.pi C :=
  by
  ext1 f
  simp only [squareCylinders, mem_iUnion, mem_image, mem_univ_pi, mem_setOf_eq, eq_comm (a := f)]

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