English
Let {t_i} be a directed family of intermediate fields of L over K. Then the underlying set of the supremum equals the union of the underlying sets of the members: ↑(iSup t) = ⋃ i (t_i : Set L).
Русский
Пусть {t_i} — направленная семейство промежуточных полей L/K. Тогда множество, лежащее внизу над их верхом, совпадает с объединением множеств каждого члена: ↑(iSup t) = ⋃ i (t_i : Set L).
LaTeX
$$$\uparrow(\mathrm{iSup}\ t) = \bigcup_{i} (t_i : \mathrm{Set} \ L)$$$
Lean4
theorem coe_iSup_of_directed [Nonempty ι] (dir : Directed (· ≤ ·) t) : ↑(iSup t) = ⋃ i, (t i : Set L) :=
let M : IntermediateField K L :=
{ __ := Subalgebra.copy _ _ (Subalgebra.coe_iSup_of_directed dir).symm
inv_mem' := fun _ hx ↦
have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
Set.mem_iUnion.mpr ⟨i, (t i).inv_mem hi⟩ }
have : iSup t = M :=
le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (t i : Set L)) i) (Set.iUnion_subset fun _ ↦ le_iSup t _)
this.symm ▸ rfl
