isOpen_iff_of_mem — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpen_iff_of_mem (h : ∞ ∈ s) : IsOpen s ↔ IsClosed ((↑) ⁻¹' s : Set X)ᶜ ∧ IsCompact ((↑) ⁻¹' s : Set X)ᶜ := by
  simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]

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