isOpen_Iio

Mathlib.Topology.Algebra.WithZeroTopology

URI: https://scilib.ai/kg/mathlib#WithZeroTopology.isOpen_Iio

English

Any Iio(a) with a ∈ Γ₀ is open in this topology.

Русский

Любой Iio(a) с а ∈ Γ₀ является открытым в этой топологии.

LaTeX

$$$\text{IsOpen}(Iio(a)) \, (\text{for any }a)$$$

Lean4

theorem isOpen_Iio {a : Γ₀} : IsOpen (Iio a) :=
  isOpen_iff.mpr <| imp_iff_not_or.mp fun ha => ⟨a, ne_of_gt ha, Subset.rfl⟩

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

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

Разделы

Аффилиация

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