isOpen_iff_of_notMem

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.isOpen_iff_of_notMem

English

If ∞ ∉ s, then IsOpen s is equivalent to IsOpen i^{-1}(s).

Русский

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

LaTeX

$$$IsOpen(s) \\iff IsOpen(i^{-1}(s)).$$$

Lean4

theorem isOpen_iff_of_notMem (h : ∞ ∉ s) : IsOpen s ↔ IsOpen ((↑) ⁻¹' s : Set X) := by simp [isOpen_def, h]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru