English
The supremum of a nonempty set of intermediate fields, viewed as a subfield, equals the supremum of their images under toSubfield.
Русский
Верхняя граница непустого множества промежуточных полей, как подполья, равна верхней границе их изображений в подпольях.
LaTeX
$$$ (sSup S).toSubfield = sSup (toSubfield '' S) \\quad (S.Nonempty) $$$
Lean4
@[simp]
theorem sSup_toSubfield (S : Set (IntermediateField F E)) (hS : S.Nonempty) :
(sSup S).toSubfield = sSup (toSubfield '' S) :=
by
have h : toSubfield '' S = Subfield.closure '' (SetLike.coe '' S) :=
by
rw [Set.image_image]
congr! with x
exact x.toSubfield.closure_eq.symm
rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_toSubfield]
congr 1
rw [Set.union_eq_right]
rintro _ ⟨x, rfl⟩
obtain ⟨y, hy⟩ := hS
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]
exact ⟨y, hy, algebraMap_mem y x⟩
