of_comp — Mathlib

English

Let (nhds x).HasBasis p s. Then MapClusterPt x F u is equivalent to ∀ i, p i → frequently a ∈ F with u a ∈ s_i.

Русский

Пусть (nhds x) имеет базис p i s_i. Тогда MapClusterPt x F u эквивалентно ∀ i, p i → ∃ᶠ a в F, u a ∈ s_i.

LaTeX

$$$\\bigl( (\\mathcal{N}x).HasBasis p s \\bigr) \\Rightarrow\\ \\mathrm{MapClusterPt}(x,F,u) \\iff \\forall i, p(i) \\rightarrow \\exists^\\mathrm{freq} a \\in F,\\; u(a) \\in s_i$$$

Lean4

theorem of_comp {φ : β → α} {p : Filter β} (h : Tendsto φ p F) (H : MapClusterPt x p (u ∘ φ)) : MapClusterPt x F u :=
  H.clusterPt.mono <| map_mono h

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