isSeparable_iSup — Mathlib

English

The supremum of a family of separable extensions is separable (auxiliary lemma).

Русский

Супремум семейства сепарабельных расширений является сепарабельным (помощь).

LaTeX

$$$\\text{IsSeparable}_F\\left(\\bigsqcup_i t_i\\right)$$$

Lean4

/-- A compositum of separable extensions is separable. -/
instance isSeparable_iSup {ι : Type*} {t : ι → IntermediateField F E} [h : ∀ i, Algebra.IsSeparable F (t i)] :
    Algebra.IsSeparable F (⨆ i, t i : IntermediateField F E) :=
  by
  simp_rw [← le_separableClosure_iff] at h ⊢
  exact iSup_le h

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