multipliable_iff_tendsto_cofinite_one

English

Same as above: Multipliable f iff Tendsto f cofinite (nhds 1).

Русский

То же самое: умножимость f эквивалентна стремлению f к 1 по кофинитному фильтру.

LaTeX

$$$\\displaystyle \\text{Multipliable}(f) \\iff \\text{Tendsto}(f,\\text{cofinite},(\\mathcal{nhds} 1))$$$

Lean4

/-- Let `G` be a complete nonarchimedean multiplicative abelian group. Then a function `f : α → G`
is unconditionally multipliable if and only if it tends to one on the filter of cofinite sets. -/
@[to_additive /-- Let `G` be a complete nonarchimedean additive abelian group. Then a function
    `f : α → G` is unconditionally summable if and only if it tends to zero on the filter of cofinite
    sets. -/
    ]
theorem multipliable_iff_tendsto_cofinite_one [CompleteSpace G] (f : α → G) :
    Multipliable f ↔ Tendsto f cofinite (𝓝 1) :=
  ⟨Multipliable.tendsto_cofinite_one, multipliable_of_tendsto_cofinite_one⟩

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