empty_mem_closedCompactCylinders — Mathlib

English

The empty set is a member of the closed-compact cylinder family for any index system X.

Русский

Пусть множество пусто, тогда пустое множество принадлежит множеству цилиндров, образованных из замкнутых компактных оснований.

LaTeX

$$$$\\emptyset \\in \\text{closedCompactCylinders}(X).$$$$

Lean4

theorem empty_mem_closedCompactCylinders : ∅ ∈ closedCompactCylinders X :=
  by
  simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff]
  exact ⟨∅, ∅, isClosed_empty, isCompact_empty, (cylinder_empty _).symm⟩

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