tendsto_iff_forall_eval_tendsto — Mathlib

English

If B is injective, the map x ↦ (y ↦ B(x,y)) is an embedding, i.e., a homeomorphism onto its image when restricted to WeakBilin B.

Русский

Если B инъективно, отображение x ↦ (y ↦ B(x,y)) является встраиванием, то есть тождественно сферическое отображение на образ при ограничении на WeakBilin B.

LaTeX

$$IsEmbedding (fun (x : WeakBilin B) y => B x y) under injectivity of B$$

Lean4

theorem tendsto_iff_forall_eval_tendsto {l : Filter α} {f : α → WeakBilin B} {x : WeakBilin B}
    (hB : Function.Injective B) : Tendsto f l (𝓝 x) ↔ ∀ y, Tendsto (fun i => B (f i) y) l (𝓝 (B x y)) :=
  by
  rw [← tendsto_pi_nhds, (isEmbedding hB).tendsto_nhds_iff]
  rfl

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