isTotallyReal_iSup — Mathlib

English

If each k_i is totally real, then their supremum iSup_i k_i is totally real.

Русский

Если каждый k_i полностью вещественный, то их верхняя сумма iSup_i k_i полностью вещественна.

LaTeX

$$$\big( \forall i, \text{IsTotallyReal}(k_i) \big) \Rightarrow \text{IsTotallyReal}\left( \bigsqcup_i k_i \right)$$$

Lean4

instance isTotallyReal_iSup {ι : Type*} {k : ι → Subfield K} [∀ i, IsTotallyReal (k i)] :
    IsTotallyReal (⨆ i, k i : Subfield K) := by simp_all [isTotallyReal_iff_le_maximalRealSubfield]

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