iInf_span_singleton — Mathlib

English

Let I_i be a family of elements of R with pairwise coprimality. Then the infimum over i of span({I_i}) equals span of the product ∏ I_i.

Русский

Пусть I_i — семейство элементов R попарно взаимно простых; тогда $\\bigwedge_i \\operatorname{span}(\{I_i\}) = \\operatorname{span}(\\prod_i I_i)$.

LaTeX

$$$\\bigwedge_{i} \\operatorname{span}(\\{I(i)\\}) = \\operatorname{span}\\left(\\prod_{i} I(i)\\right)$$$

Lean4

theorem iInf_span_singleton {ι : Type*} [Fintype ι] {I : ι → R} (hI : ∀ (i j) (_ : i ≠ j), IsCoprime (I i) (I j)) :
    ⨅ i, span ({I i} : Set R) = span {∏ i, I i} :=
  by
  rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]
  rwa [Finset.coe_univ, Set.pairwise_univ]

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