MapClusterPt — Mathlib

English

A point x is a cluster point of a sequence u along a filter F if it is a cluster point of map u F.

Русский

Точка x является кластерной точкой последовательности u вдоль фильтра F, если она кластерная точка образа map u F.

LaTeX

$$$\operatorname{MapClusterPt}(x,F,u) \iff \operatorname{ClusterPt}(x,\operatorname{map}uF)$$$

Lean4

/-- A point `x` is a cluster point of a sequence `u` along a filter `F` if it is a cluster point
of `map u F`. -/
def MapClusterPt {ι : Type*} (x : X) (F : Filter ι) (u : ι → X) : Prop :=
  ClusterPt x (map u F)

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