cylinder_empty

Mathlib.MeasureTheory.Constructions.Cylinders

URI: https://scilib.ai/kg/mathlib#MeasureTheory.cylinder_empty

English

For any finite set s, the cylinder over the empty base is empty.

Русский

Для любого конечного множества s цилиндр над пустым основанием равен пустому множеству.

LaTeX

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

Lean4

@[simp]
theorem cylinder_empty (s : Finset ι) : cylinder s (∅ : Set (∀ i : s, α i)) = ∅ := by rw [cylinder, preimage_empty]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru