mem_closedCompactCylinders — Mathlib

English

A set t lies in closedCompactCylinders X if and only if there exist a finite index set s and a closed compact base S with t = cylinder(s,S).

Русский

Множество t принадлежит closedCompactCylinders X тогда и только тогда, когда существуют конечный набор индексов s и замкнутая компактная база S с t = cylinder(s,S).

LaTeX

$$$$t \\in \\text{closedCompactCylinders}(X) \\iff \\exists s,S,\\ IsClosed(S) \\wedge \\ IsCompact(S) \\wedge t = \\mathrm{cylinder}(s,S).$$$$

Lean4

theorem mem_closedCompactCylinders (t : Set (Π i, X i)) :
    t ∈ closedCompactCylinders X ↔ ∃ (s S : _), IsClosed S ∧ IsCompact S ∧ t = cylinder s S := by
  simp_rw [closedCompactCylinders, mem_iUnion, mem_singleton_iff, exists_prop]

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