mem_interior

Mathlib.Topology.Sets.Opens

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

English

x belongs to Opens.interior s iff x belongs to interior s.

Русский

x принадлежит Opens.interior s тогда и только тогда, когда x принадлежит interior(s).

LaTeX

$$$x \in \mathrm{Opens.interior}(s) \iff x \in \operatorname{interior}(s)$$$

Lean4

@[simp]
theorem mem_interior {s : Set α} {x : α} : x ∈ Opens.interior s ↔ x ∈ _root_.interior s :=
  .rfl

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

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

Разделы

Аффилиация

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