cylinder_univ — Mathlib

English

For any finite set s, the cylinder over the universal base is all functions, i.e., the whole space.

Русский

Для любого конечного множества s цилиндр над всеобъемлющей базой даёт всё пространство.

LaTeX

$$$$\\mathrm{cylinder}(s, \\mathrm{univ}) = \\mathrm{univ}.$$$$

Lean4

@[simp]
theorem cylinder_univ (s : Finset ι) : cylinder s (univ : Set (∀ i : s, α i)) = univ := by rw [cylinder, preimage_univ]

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