prod_sup_eq_top — Mathlib

English

Let s be a finite set and J i ideals of R. If for all i ∈ s we have J_i ⊔ I = ⊤, then (∏ i ∈ s J_i) ⊔ I = ⊤.

Русский

Пусть s — конечный набор, и J_i — идеалы R; если для каждого i ∈ s выполнено J_i ⊔ I = ⊤, тогда (∏ i∈s J_i) ⊔ I = ⊤.

LaTeX

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

Lean4

theorem prod_sup_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → J i ⊔ I = ⊤) : (∏ i ∈ s, J i) ⊔ I = ⊤ := by
  rw [sup_comm, sup_prod_eq_top]; intro i hi; rw [sup_comm, h i hi]

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