multipliable_iff_cauchySeq_finset

English

For a fixed f, f is multipliable iff both restrictions to a subset s and its complement are multipliable.

Русский

Для заданной функции f умножаемость эквивалентна тому, что она умножаема и на s, и на его дополнение.

LaTeX

$$$\text{Multipliable}(f) \iff (\text{Multipliable}(f|_s) \land \text{Multipliable}(f|_{\,\beta\setminus s})).$$$

Lean4

/-- The **Cauchy criterion** for infinite products, also known as the **Cauchy convergence test** -/
@[to_additive /-- The **Cauchy criterion** for infinite sums, also known as the
    **Cauchy convergence test** -/
    ]
theorem multipliable_iff_cauchySeq_finset [CompleteSpace α] {f : β → α} :
    Multipliable f ↔ CauchySeq fun s : Finset β ↦ ∏ b ∈ s, f b := by classical exact cauchy_map_iff_exists_tendsto.symm

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