clusterPt_comap — Mathlib

English

If f is open and l is a filter on Y with a cluster point at f(x), then x is a cluster point for comap f l.

Русский

Если f открытое отображение и l — фильтр на Y с кластерной точкой в f(x), то x является кластерной точкой для comap f l.

LaTeX

$$$$IsOpenMap(f) \\rightarrow \\forall x, \\forall l, ClusterPt(f(x), l) \\rightarrow ClusterPt(x, comap f l)$$$$

Lean4

theorem clusterPt_comap (hf : IsOpenMap f) {x : X} {l : Filter Y} (h : ClusterPt (f x) l) : ClusterPt x (comap f l) :=
  by
  rw [ClusterPt, ← map_neBot_iff, Filter.push_pull]
  exact h.neBot.mono <| inf_le_inf_right _ <| hf.nhds_le _

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