English
If S is a nonempty directed set of subfields of K, then x lies in the supremum ⨆ i, S_i exactly when x lies in some S_i.
Русский
Пусть S — непустое направленное множество подполей K. Тогда x ∈ ⨆_i S_i тогда и только тогда, когда ∃ i: x ∈ S_i.
LaTeX
$$$ x \in \bigvee_{i} S(i) \;\iff\; \exists i,\; x \in S(i) $$$
Lean4
/-- The underlying set of a non-empty directed sSup of subfields is just a union of the subfields.
Note that this fails without the directedness assumption (the union of two subfields is
typically not a subfield) -/
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) {x : K} :
(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i :=
by
let s : Subfield K :=
{ __ := Subring.copy _ _ (Subring.coe_iSup_of_directed hS).symm
inv_mem' := fun _ hx ↦
have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
Set.mem_iUnion.mpr ⟨i, (S i).inv_mem hi⟩ }
have : iSup S = s :=
le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
exact this ▸ Set.mem_iUnion
