sup_iInf_eq_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem sup_iInf_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → I ⊔ J i = ⊤) : (I ⊔ ⨅ i ∈ s, J i) = ⊤ :=
  by
  rw [eq_top_iff, ← sup_prod_eq_top h, ← Finset.inf_eq_iInf]
  grw [prod_le_inf]

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