diff_mem_nhdsWithin_compl

Mathlib.Topology.ContinuousOn

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

English

If s ∈ nhds x, then s \ t ∈ nhdsWithin x (t^c) for any t.

Русский

Если s ∈ nhds x, то s \ t ∈ nhdsWithin x (t^c) для любого t.

LaTeX

$$$s ∈ 𝓝 x \Rightarrow ∀ t, \ s \ t ∈ 𝓝[t^c] x$$$

Lean4

theorem diff_mem_nhdsWithin_compl {x : α} {s : Set α} (hs : s ∈ 𝓝 x) (t : Set α) : s \ t ∈ 𝓝[tᶜ] x :=
  diff_mem_inf_principal_compl hs t

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

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

Разделы

Аффилиация

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