mapClusterPt_iff — Mathlib

English

For inducing f, MapClusterPt (f x) l f holds iff ClusterPt x l holds.

Русский

Для индуциирующего f имеет место эквивалентность MapClusterPt (f x) l f и ClusterPt x l.

LaTeX

$$$\operatorname{MapClusterPt}(f(x), l, f) \iff \operatorname{ClusterPt}(x, l).$$$

Lean4

theorem mapClusterPt_iff (hf : IsInducing f) {x : X} {l : Filter X} : MapClusterPt (f x) l f ↔ ClusterPt x l :=
  by
  delta MapClusterPt ClusterPt
  rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]

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