inseparable_of_nhdsWithin_eq — Mathlib

English

If x and y belong to a set s and their nhdsWithin at x and y with respect to s are equal, then x and y are inseparable.

Русский

Если x,y∈s и nhdsWithin x s = nhdsWithin y s, то x и y неразделимы.

LaTeX

$$$x \\in s \\land y \\in s \\land h : 𝓝[s] x = 𝓝[s] y \\\\Rightarrow x \\sim_i y.$$$

Lean4

theorem inseparable_of_nhdsWithin_eq (hx : x ∈ s) (hy : y ∈ s) (h : 𝓝[s] x = 𝓝[s] y) : x ~ᵢ y :=
  (specializes_of_nhdsWithin h.le hx).antisymm (specializes_of_nhdsWithin h.ge hy)

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