inter_mem_nhdsWithin

Mathlib.Topology.ContinuousOn

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

English

If t is a neighborhood of a, then s ∩ t is a neighborhood of a within s.

Русский

Если t — окрестность a, то s ∩ t является окрестностью a внутри s.

LaTeX

$$$ t \in \mathcal{N}(a) \Rightarrow s \cap t \in \mathcal{N}_s(a) $$$

Lean4

theorem inter_mem_nhdsWithin (s : Set α) {t : Set α} {a : α} (h : t ∈ 𝓝 a) : s ∩ t ∈ 𝓝[s] a :=
  inter_mem self_mem_nhdsWithin (mem_inf_of_left h)

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

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

Разделы

Аффилиация

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