tendsto_lift_nhdsWithin_mk — Mathlib

English

Tendsto (lift f hf) (nhdsWithin (mk x) s) l is equivalent to Tendsto f (nhdsWithin x (mk^{-1}' s)) l.

Русский

Tendsto (lift f hf) (nhdsWithin (mk x) s) l ⇔ Tendsto f (nhdsWithin x (mk^{-1}' s)) l.

LaTeX

$$Tendsto (lift f hf) (nhdsWithin (mk x) s) l ↔ Tendsto f (nhdsWithin x (mk^{-1}' s)) l$$

Lean4

@[simp]
theorem tendsto_lift_nhdsWithin_mk {f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)}
    {l : Filter α} : Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l := by
  simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]

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