tendsto_subtype_rng — Mathlib

English

Map along the inclusion from the subtype to the ambient space sends the neighborhood filter to the neighborhood filter of the ambient point.

Русский

Отображение через включение подтипа в пространство осмысляет окрестностный фильтр точке в пространстве.

LaTeX

$$$\text{map}((\uparrow): {x//p x} \to X)(\mathcal{N}⟨x, hx⟩) = \mathcal{N} x$$$

Lean4

theorem tendsto_subtype_rng {Y : Type*} {p : X → Prop} {l : Filter Y} {f : Y → Subtype p} :
    ∀ {x : Subtype p}, Tendsto f l (𝓝 x) ↔ Tendsto (fun x => (f x : X)) l (𝓝 (x : X))
  | ⟨a, ha⟩ => by rw [nhds_subtype_eq_comap, tendsto_comap_iff]; rfl

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