isClosed_iff_of_mem — Mathlib

English

If ∞ ∈ s, then IsClosed s is equivalent to IsClosed i^{-1}(s) ∧ IsCompact i^{-1}(s).

Русский

Если ∞ ∈ s, то IsClosed s эквивалентно IsClosed i^{-1}(s) ∧ IsCompact i^{-1}(s).

LaTeX

$$$IsClosed(s) \\iff IsClosed(i^{-1}(s)) \\land IsCompact(i^{-1}(s)).$$$

Lean4

theorem isClosed_iff_of_mem (h : ∞ ∈ s) : IsClosed s ↔ IsClosed ((↑) ⁻¹' s : Set X) :=
  by
  have : ∞ ∉ sᶜ := fun H => H h
  rw [← isOpen_compl_iff, isOpen_iff_of_notMem this, ← isOpen_compl_iff, preimage_compl]

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