nhdsWithin_target_inter

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.nhdsWithin_target_inter

English

For x in the target, the nhdsWithin of x w.r.t. e.target ∩ s equals the nhdsWithin of s.

Русский

Для x в целевой области, 𝓝[ e.target ∩ s ] x = 𝓝[ s ] x.

LaTeX

$$$\forall x\in e.target, 𝓝[e.target \cap s] x = 𝓝[s] x$$$

Lean4

theorem nhdsWithin_target_inter {x} (hx : x ∈ e.target) (s : Set Y) : 𝓝[e.target ∩ s] x = 𝓝[s] x :=
  e.symm.nhdsWithin_source_inter hx s

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

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

Разделы

Аффилиация

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