multipliable_iff_vanishing — Mathlib

English

Equivalent reformulation of the Cauchy criterion for tprod in terms of sets rather than Finsets.

Русский

Эквивалентное переформулирование критерия Коши для tprod через множества вместо конечных подмножеств.

LaTeX

$$$(\text{CauchySeq} \; (s \mapsto \prod_{b\in s} f(b))) \iff \forall e \in \mathcal{N}(1), \exists s, \forall t \subseteq \text{β}, \text{Disjoint}(t,s) \Rightarrow (\prod_{b\in t} f(b)) \in e.$$$

Lean4

@[to_additive]
theorem multipliable_iff_vanishing :
    Multipliable f ↔ ∀ e ∈ 𝓝 (1 : α), ∃ s : Finset β, ∀ t, Disjoint t s → (∏ b ∈ t, f b) ∈ e := by
  rw [multipliable_iff_cauchySeq_finset, cauchySeq_finset_iff_prod_vanishing]

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