isOpen_sigma_iff

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#isOpen_sigma_iff

English

The range of the i-th Sigma.mk is an open subset of the sigma type.

Русский

Образ i-й инъекции Sigma.mk i является открытым подмножеством суммы.

LaTeX

$$$\\text{IsOpen}(\\operatorname{range}(\\Sigma.mk\\ i))$$$

Lean4

theorem isOpen_sigma_iff {s : Set (Sigma σ)} : IsOpen s ↔ ∀ i, IsOpen (Sigma.mk i ⁻¹' s) :=
  by
  rw [isOpen_iSup_iff]
  rfl

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

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

Разделы

Аффилиация

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