F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
key : adjoin F ↑S = ⨆ (x : E) (_ : x ∈ S), F⟮x⟯
⊢ IsCompactElement (adjoin F ↑S)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
⊢ IsCompactElement (adjoin F ↑S)
have key : adjoin F ↑S = ⨆ x ∈ S, F⟮x⟯ := by
refine' le_antisymm (adjoin_le_iff.mpr fun x hx => SetLike.mem_coe.mpr
    (adjoin_simple_le_iff.mp (le_iSup_of_le x (le_iSup_iff.2 (fun E1 hE1 => hE1 hx)))))
      (iSup_le fun x => iSup_le fun hx =>  adjoin_simple_le_iff.mpr (subset_adjoin F S hx))
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
key : adjoin F ↑S = ⨆ (x : E) (_ : x ∈ S), F⟮x⟯
⊢ IsCompactElement (Finset.sup S fun x => F⟮x⟯)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
key : adjoin F ↑S = ⨆ (x : E) (_ : x ∈ S), F⟮x⟯
⊢ IsCompactElement (adjoin F ↑S)
rw [key, ← Finset.sup_eq_iSup]
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
key : adjoin F ↑S = ⨆ (x : E) (_ : x ∈ S), F⟮x⟯
⊢ IsCompactElement (Finset.sup S fun x => F⟮x⟯)
exact finset_sup_compact_of_compact S fun x _ => adjoin_simple_isCompactElement x
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
S✝ : Set E
α : E
S : Finset E
⊢ adjoin F ↑S = ⨆ (x : E) (_ : x ∈ S), F⟮x⟯
refine' le_antisymm (adjoin_le_iff.mpr fun x hx => SetLike.mem_coe.mpr
  (adjoin_simple_le_iff.mp (le_iSup_of_le x (le_iSup_iff.2 (fun E1 hE1 => hE1 hx)))))
    (iSup_le fun x => iSup_le fun hx =>  adjoin_simple_le_iff.mpr (subset_adjoin F S hx))