isOpen_iInter

Mathlib.Topology.AlexandrovDiscrete

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

English

If a family f i of sets is open for every index i, then their indexed intersection is open.

Русский

Если для каждого индекса i множество f_i открыто, то их пересечение по индексу i открыто.

LaTeX

$$$\Big(\forall i, IsOpen(f(i))\Big) \Rightarrow IsOpen(\bigcap_i f(i))$$$

Lean4

theorem isOpen_iInter (hf : ∀ i, IsOpen (f i)) : IsOpen (⋂ i, f i) :=
  isOpen_sInter <| forall_mem_range.2 hf

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

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

Разделы

Аффилиация

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