pure_le_nhdsWithin

Mathlib.Topology.ContinuousOn

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

English

The pure neighborhood of a point lies below the nhdsWithin neighborhood when a ∈ s.

Русский

Чистая окрестность точки лежит ниже nhdsWithin, когда a ∈ s.

LaTeX

$$$ a \in s \Rightarrow pure(a) \le \mathcal{N}_s(a) $$$

Lean4

theorem pure_le_nhdsWithin {a : α} {s : Set α} (ha : a ∈ s) : pure a ≤ 𝓝[s] a :=
  le_inf (pure_le_nhds a) (le_principal_iff.2 ha)

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

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

Разделы

Аффилиация

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