tendsto_support_normed_smallSets — Mathlib

English

In a proper space, a closed ball is compact: IsCompact(Metric.closedBall(x,r)).

Русский

В правильном метрическом пространстве любой замкнутый шар компактен: IsCompact(Metric.closedBall(x,r)).

LaTeX

$$$ \operatorname{IsCompact}(\mathrm{Metric}.closedBall(x,r)) $$$

Lean4

theorem tendsto_support_normed_smallSets {ι} {φ : ι → ContDiffBump c} {l : Filter ι}
    (hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)) :
    Tendsto (fun i => Function.support fun x => (φ i).normed μ x) l (𝓝 c).smallSets :=
  by
  simp_rw [NormedAddCommGroup.tendsto_nhds_zero, Real.norm_eq_abs, abs_eq_self.mpr (φ _).rOut_pos.le] at hφ
  rw [nhds_basis_ball.smallSets.tendsto_right_iff]
  refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_
  rw [(φ i).support_normed_eq]
  exact ball_subset_ball hi.le

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