nhdsWithin_le_iff — Mathlib

English

Relationship between the order of neighborhood filters: 𝒩_s(x) ≤ 𝒩_t(x) iff t ∈ 𝒩_s(x).

Русский

Соотношение порядка окрестностей: 𝒩_s(x) ≤ 𝒩_t(x) тогда и только тогда, когда t ∈ 𝒩_s(x).

LaTeX

$$$ \mathcal{N}_s(x) \le \mathcal{N}_t(x) \iff t \in \mathcal{N}_s(x) $$$

Lean4

theorem nhdsWithin_le_iff {s t : Set α} {x : α} : 𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x :=
  set_eventuallyLE_iff_inf_principal_le.symm.trans set_eventuallyLE_iff_mem_inf_principal

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