nhdsWithin_eq_nhdsWithin — Mathlib

English

If a ∈ s and s is open, and t ∩ s = u ∩ s, then 𝓝[t] a = 𝓝[u] a.

Русский

Если a ∈ s и s открыто, и t ∩ s = u ∩ s, тогда 𝓝[t] a = 𝓝[u] a.

LaTeX

$$$ s \in \mathcal{N}(a) \land IsOpen s \Rightarrow 𝓝[t] a = 𝓝[u] a \text{ при } t \cap s = u \cap s $$$

Lean4

theorem nhdsWithin_eq_nhdsWithin {a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s) (h₂ : t ∩ s = u ∩ s) :
    𝓝[t] a = 𝓝[u] a := by rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]

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