mapClusterPt — Mathlib

English

The equivalence mapClusterPt x F u ↔ clusterPt x (map u F) holds, i.e., the concept is invariant under definitional rewriting of maps.

Русский

Справедлива эквивалентность MapClusterPt x F u ↔ ClusterPt x (map u F), то есть понятие не изменяется при замене отображения на эквивалентное.

LaTeX

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

Lean4

theorem mapClusterPt [NeBot F] (h : Tendsto u F (𝓝 x)) : MapClusterPt x F u :=
  .of_le_nhds h

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