insert_mem_nhdsWithin_of_subset_insert

English

If t is contained in insert y s, then insert x s belongs to nhdsWithin x t.

Русский

Если t ⊆ insert y s, тогда insert x s ∈ nhdsWithin x t.

LaTeX

$$$t \subseteq insert\ y\ s \Rightarrow insert\ x\ s \in \mathcal{N}\!\!_{x}(t).$$$

Lean4

/-- If `t` is a subset of `s`, except for one point,
then `insert x s` is a neighborhood of `x` within `t`. -/
theorem insert_mem_nhdsWithin_of_subset_insert [T1Space X] {x y : X} {s t : Set X} (hu : t ⊆ insert y s) :
    insert x s ∈ 𝓝[t] x := by
  rcases eq_or_ne x y with (rfl | h)
  · exact mem_of_superset self_mem_nhdsWithin hu
  refine nhdsWithin_mono x hu ?_
  rw [nhdsWithin_insert_of_ne h]
  exact mem_of_superset self_mem_nhdsWithin (subset_insert x s)

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