le_nhds_of_str_eq — Mathlib

English

If X.str F = x, then F ≤ nhds x (in the ultrafilter order).

Русский

Если X.str F = x, то F ≤ nhds x (в порядке ультрафильтров).

LaTeX

$$$X.str F = x \\Rightarrow F \\le \\ nhds x$$$

Lean4

theorem le_nhds_of_str_eq {X : Compactum} (F : Ultrafilter X) (x : X) : X.str F = x → ↑F ≤ 𝓝 x := fun h =>
  le_nhds_iff.mpr fun s hx hs =>
    hs _ <| by
      rwa [h]
        -- All the hard work above boils down to this `T2Space` instance.

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