mono — Mathlib

English

If f tends to y along nhds x and x has a MapClusterPt x F u, then MapClusterPt y F (f ∘ u).

Русский

Если f стремится к y по отношению к nhds x и есть MapClusterPt x F u, то MapClusterPt y F (f ∘ u).

LaTeX

$$$\\operatorname{Tendsto} f (\\mathcal{N}(x)) (\\mathcal{N}(y)) \\wedge \\mathrm{MapClusterPt}(x,F,u) \\Rightarrow \\mathrm{MapClusterPt}(y,F,f\\circ u)$$$

Lean4

theorem mono {G : Filter α} (h : MapClusterPt x F u) (hle : F ≤ G) : MapClusterPt x G u :=
  h.clusterPt.mono (map_mono hle)

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