diff_mem_nhdsWithin_diff

Mathlib.Topology.ContinuousOn

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

← MathLib Explorer

English

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

Русский

Если s ∈ nhds x, то s \ t' ∈ nhdsWithin x (t'^c).

LaTeX

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

Lean4

theorem diff_mem_nhdsWithin_diff {x : α} {s t : Set α} (hs : s ∈ 𝓝[t] x) (t' : Set α) : s \ t' ∈ 𝓝[t \ t'] x :=
  by
  rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]
  exact inter_mem_inf hs (mem_principal_self _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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