variables_tendsto_zero — Mathlib

English

The family X i tends to zero in the pi-topology; more precisely, the map X· : σ → MvPowerSeries σ R tends to 0 cofinitely.

Русский

Семейство переменных X_i сходится к нулю в топологии Pi; конкретно X· стремится к 0 по кофинитному фильтру.

LaTeX

$$Tendsto (X · : σ → MvPowerSeries σ R) cofìnite (nhds 0)$$

Lean4

theorem variables_tendsto_zero [Semiring R] : Tendsto (X · : σ → MvPowerSeries σ R) cofinite (nhds 0) := by
  classical
  simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]
  refine fun d ↦ tendsto_nhds_of_eventually_eq ?_
  by_cases h : ∃ i, d = Finsupp.single i 1
  · obtain ⟨i, hi⟩ := h
    filter_upwards [eventually_cofinite_ne i] with j hj
    simp [hi, Finsupp.single_eq_single_iff, hj.symm]
  · simpa only [ite_eq_right_iff] using Eventually.of_forall fun x h' ↦ (not_exists.mp h x h').elim

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