English
The carrier of the supremum of a directed family equals the union of the carriers: ((⨆ i, S_i) : Set R) = ⋃ i, S_i.
Русский
Носитель верхнего предела направленного семейства равен объединению носителей: ((⨆ i, S_i) : Set R) = ⋃ i, S_i.
LaTeX
$$$ ((\bigvee_i S_i) : Set R) = \bigcup_i S_i $$$
Lean4
/-- The underlying set of a non-empty directed sSup of subrings is just a union of the subrings.
Note that this fails without the directedness assumption (the union of two subrings is
typically not a subring) -/
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (· ≤ ·) S) {x : R} :
(x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i := by
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
let U : Subring R :=
Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
(Submonoid.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)
suffices ⨆ i, S i ≤ U by simpa [U] using @this x
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩
