sup_prod_eq_top — Mathlib

English

Let I be an ideal and J i : ι → Ideal R. If for all i, i ∈ s we have I ⊔ J i = ⊤, then I ⊔ ∏ i ∈ s J i = ⊤.

Русский

Пусть I — идеал, и для суммы J_i ограничение над i ∈ s: если для всех i ∈ s выполняется I ⊔ J_i = ⊤, то I ⊔ (∏ i∈s J_i) = ⊤.

LaTeX

$$$ \bigl( I \Bigr) \oplus ( \prod_{i \in s} J_i ) = \top \quad \text{при } \forall i \in s, I \oplus J_i = \top. $$$

Lean4

theorem sup_prod_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → I ⊔ J i = ⊤) : (I ⊔ ∏ i ∈ s, J i) = ⊤ :=
  Finset.prod_induction _ (fun J => I ⊔ J = ⊤) (fun _ _ hJ hK => (sup_mul_eq_of_coprime_left hJ).trans hK)
    (by simp_rw [one_eq_top, sup_top_eq]) h

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