eventually_bounded_finset_prod — Mathlib

English

In a complete normed ring, if the sum of norms ∑‖f_i‖ converges, then ∏′ (1+f_i) converges (multipliable).

Русский

В полном нормированном кольце, если сумма норм ∑‖f_i‖ сходится, то ∏′ (1+f_i) сходится (существует).

LaTeX

$$$\prod'_{i} (1 + f_i) \text{ converges}$$$

Lean4

theorem eventually_bounded_finset_prod {v : ι → ℝ} (hv : Multipliable v) :
    ∃ r₁ > 0, ∃ s₁, ∀ t, s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁ :=
  by
  obtain ⟨r₁, hr₁⟩ := exists_gt (max 0 <| ∏' i, v i)
  rw [max_lt_iff] at hr₁
  have := hv.hasProd.eventually_le_const hr₁.2
  rw [unconditional, eventually_atTop] at this
  refine ⟨r₁, hr₁.1, this⟩

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