isIntegral_iSup — Mathlib

English

Let (S_i) be a family of subalgebras of A over R. The supremum iSup_i S_i is integral over R if and only if every S_i is integral over R.

Русский

Пусть (S_i) — семейство подалгебр A над R. Наибольшая полуобъединение iSup_i S_i интегральна над R тогда и только тогда, когда каждый S_i интегральен над R.

LaTeX

$$$IsIntegral R \left(\iSup_{i} S(i)\right) \iff \forall i, IsIntegral R (S(i))$$$

Lean4

theorem isIntegral_iSup {ι} (S : ι → Subalgebra R A) :
    Algebra.IsIntegral R ↑(iSup S) ↔ ∀ i, Algebra.IsIntegral R (S i) := by
  simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]

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