mem_nhds_subtype_iff_nhdsWithin

Mathlib.Topology.ContinuousOn

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

← MathLib Explorer

English

For a subtype a ∈ s, t ∈ nhds a iff (↑) '' t ∈ nhdsWithin a.val s.

Русский

Для подтипа a ∈ s: t ∈ nhds a эквивалентно (↑) '' t ∈ nhdsWithin a.val s.

LaTeX

$$$ t \in 𝓝 a \iff (↑) '' t \in 𝓝[s] (a.val) $$$

Lean4

theorem mem_nhds_subtype_iff_nhdsWithin {s : Set α} {a : s} {t : Set s} : t ∈ 𝓝 a ↔ (↑) '' t ∈ 𝓝[s] (a : α) := by
  rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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