isPurelyInseparable_sup — Mathlib

English

A supremum (iSup) of purely inseparable extensions is again purely inseparable.

Русский

Супремум (iSup) чисто бесразделимых расширений снова чисто бесразделимо.

LaTeX

$$IsPurelyInseparable F (⨆ i, t i)$$

Lean4

/-- A compositum of two purely inseparable extensions is purely inseparable. -/
instance isPurelyInseparable_sup (L1 L2 : IntermediateField F E) [h1 : IsPurelyInseparable F L1]
    [h2 : IsPurelyInseparable F L2] : IsPurelyInseparable F (L1 ⊔ L2 : IntermediateField F E) :=
  by
  rw [← le_perfectClosure_iff] at h1 h2 ⊢
  exact sup_le h1 h2

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