nhdsWithin_inter_of_mem'

Mathlib.Topology.ContinuousOn

URI: https://scilib.ai/kg/mathlib#nhdsWithin_inter_of_mem'

English

If t is a neighborhood of a within s, then nhdsWithin a (s ∩ t) equals nhdsWithin a s.

Русский

Если t является окрестностью a внутри s, тогда nhdsWithin a (s ∩ t) = nhdsWithin a s.

LaTeX

$$$$ 𝓝[a]_{s \\cap t} = 𝓝[a]_{s} $$$$

Lean4

theorem nhdsWithin_inter_of_mem' {a : α} {s t : Set α} (h : t ∈ 𝓝[s] a) : 𝓝[s ∩ t] a = 𝓝[s] a := by
  rw [inter_comm, nhdsWithin_inter_of_mem h]

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

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

Разделы

Аффилиация

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