isTotallyReal_sup — Mathlib

English

If E and F are totally real subfields of K, then their supremum E ⊔ F is also totally real.

Русский

Если E и F — полностью вещественные подполя K, то их верхняя граница E ⊔ F тоже полностью вещественная.

LaTeX

$$$\big( \text{IsTotallyReal}(E) \land \text{IsTotallyReal}(F) \big) \Rightarrow \text{IsTotallyReal}(E \lor F)$$$

Lean4

instance isTotallyReal_sup {E F : Subfield K} [IsTotallyReal E] [IsTotallyReal F] :
    IsTotallyReal (E ⊔ F : Subfield K) := by simp_all [isTotallyReal_iff_le_maximalRealSubfield]

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