isOpen_iff_of_mem' — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{IsOpen}(s) \\iff \\big( \\infty \\in s \\to \\operatorname{IsCompact}(i^{-1}(s))^c \\big) \\wedge \\operatorname{IsOpen}(i^{-1}(s)).$$$

Lean4

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

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