mem_iSup

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.mem_iSup

English

x ∈ iSup s iff there exists i with x ∈ s i.

Русский

x принадлежит iSup s тогда, когда существует индекс i such that x ∈ s_i.

LaTeX

$$$ x \in iSup s \iff \exists i, x \in s i $$$

Lean4

@[simp]
theorem mem_iSup {ι} {x : α} {s : ι → Opens α} : x ∈ iSup s ↔ ∃ i, x ∈ s i :=
  by
  rw [← SetLike.mem_coe]
  simp

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

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

Разделы

Аффилиация

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