continuousWithinAt_lift — Mathlib

English

Tendsto (lift f hf) (nhdsWithin (mk x) s) l ↔ Tendsto f (nhdsWithin x (preimage mk s)) l.

Русский

Tendsto (lift f hf) (nhdsWithin (mk x) s) l ⇔ Tendsto f (nhdsWithin x (preimage mk s)) l.

LaTeX

$$Tendsto (lift f hf) (nhdsWithin (mk x) s) l ↔ Tendsto f (nhdsWithin x (Set.preimage mk s)) l$$

Lean4

@[simp]
theorem continuousWithinAt_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} :
    ContinuousWithinAt (lift f hf) s (mk x) ↔ ContinuousWithinAt f (mk ⁻¹' s) x :=
  tendsto_lift_nhdsWithin_mk

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