isPurelyInseparable_iSup — Mathlib

English

A supremum of a family of purely inseparable extensions is itself purely inseparable over the base field.

Русский

supremum семейства чисто неразделимых расширений над базовым полем также чисто неразделимо над этим полем.

LaTeX

$$$\text{IsPurelyInseparable } F (\bigvee_i t_i)\;\text{where each } t_i\text{ is purely inseparable over }F$$$

Lean4

/-- A compositum of purely inseparable extensions is purely inseparable. -/
instance isPurelyInseparable_iSup {ι : Sort*} {t : ι → IntermediateField F E} [h : ∀ i, IsPurelyInseparable F (t i)] :
    IsPurelyInseparable F (⨆ i, t i : IntermediateField F E) :=
  by
  simp_rw [← le_perfectClosure_iff] at h ⊢
  exact iSup_le h

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