Theorems · Theorem · field theory

IntermediateField.coe_iSup_of_directed

∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} [Nonempty ι], Directed (fun x1 x2 => x1 ≤ x2) t → ↑(iSup t) = ⋃ i, ↑(t i)

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraNonempty