isClosed_iff — Mathlib

English

A set s is closed iff either 0 ∈ s or s ⊆ Ici(γ) for some γ ≠ 0.

Русский

Множество s замкнуто тогда, когда 0 принадлежит s или существует γ ≠ 0 с s ⊆ Ici(γ).

LaTeX

$$$\text{IsClosed}(s) \iff 0 ∈ s \lor \exists γ ≠ 0, s \subseteq Ici(γ)$$$

Lean4

theorem isClosed_iff {s : Set Γ₀} : IsClosed s ↔ (0 : Γ₀) ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Ici γ := by
  simp only [← isOpen_compl_iff, isOpen_iff, mem_compl_iff, not_not, ← compl_Ici, compl_subset_compl]

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