mem_sSup

Mathlib.Topology.Sets.Opens

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

English

For a family Us, x ∈ sSup Us iff ∃ u ∈ Us with x ∈ u.

Русский

Для семейства Us: x ∈ sSup Us эквивалентно существованию u ∈ Us такое, что x ∈ u.

LaTeX

$$$ x \in sSup Us \iff \exists u \in Us, x \in u $$$

Lean4

@[simp]
theorem mem_sSup {Us : Set (Opens α)} {x : α} : x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u := by
  simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

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

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

Разделы

Аффилиация

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