specializes_of_nhdsWithin — Mathlib

English

If nhdsWithin x s ≤ nhdsWithin y s and x ∈ s, then x specializes to y.

Русский

Если nhdsWithin(x, s) ≤ nhdsWithin(y, s) и x ∈ s, тогда x специализируется на y.

LaTeX

$$$$\forall X\ [\text{TopologicalSpace } X],\ {x,y:X}\ {s:Set X},\ nhdsWithin x s \le nhdsWithin y s \rightarrow x \in s \rightarrow x \rightsquigarrow y.$$$$

Lean4

theorem specializes_of_nhdsWithin (h₁ : 𝓝[s] x ≤ 𝓝[s] y) (h₂ : x ∈ s) : x ⤳ y :=
  specializes_iff_pure.2 <|
    calc
      pure x ≤ 𝓝[s] x := le_inf (pure_le_nhds _) (le_principal_iff.2 h₂)
      _ ≤ 𝓝[s] y := h₁
      _ ≤ 𝓝 y := inf_le_left

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