extendScalars_sup — Mathlib

English

If h: F ≤ E and h': F ≤ E' are inclusions of an intermediate field F into E and E', then the join of their extensions equals the extension of the join: extendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h).

Русский

Если существует вложение F ≤ E и F ≤ E' между промежуточными полями, то объединение расширений скаляров равно расширению их объединения: extendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h).

LaTeX

$$$ (\operatorname{extendScalars} h) \;\sqcup\; (\operatorname{extendScalars} h') = \operatorname{extendScalars}(\,\operatorname{le\_sup\_of\_le\_left}(h)\,).$$$

Lean4

theorem extendScalars_sup : extendScalars h ⊔ extendScalars h' = extendScalars (le_sup_of_le_left h : F ≤ E ⊔ E') :=
  ((extendScalars.orderIso F).map_sup ⟨_, h⟩ ⟨_, h'⟩).symm

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