mem_nhdsWithin_insert

Mathlib.Topology.ContinuousOn

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

English

If t ∈ nhdsWithin a s, then insert a t ∈ nhdsWithin (insert a s) a.

Русский

Если t ∈ nhdsWithin a s, тогда insert a t ∈ nhdsWithin (insert a s) a.

LaTeX

$$$$ insert(a,t) \\in 𝓝[insert(a,s)] a $$$$

Lean4

theorem mem_nhdsWithin_insert {a : α} {s t : Set α} : t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a := by simp

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

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

Разделы

Аффилиация

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