iInf_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( \bigwedge_{i \in s} J_i \bigr) \oplus I = \top \quad \text{при } \forall i \in s, J_i \oplus I = \top. $$$

Lean4

theorem iInf_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_iInf_eq_top]; intro i hi; rw [sup_comm, h i hi]

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