English
The underlying set of a nonempty directed Sup of NonUnitalSubring R is the union of the involved Subrings: for directed S, x ∈ ⨆ i, S i iff ∃ i, x ∈ S i.
Русский
Пусть есть непустое направленное множество подполь в R; их суп ровно объединение подполь: x ∈ ⨆ i, S i ⇔ ∃ i, x ∈ S i.
LaTeX
$$$x \in \bigvee_i S_i \;\;\Leftrightarrow\;\; \exists i, x \in S_i$$$
Lean4
/-- The underlying set of a non-empty directed Sup of `NonUnitalSubring`s is just a union of the
`NonUnitalSubring`s. Note that this fails without the directedness assumption (the union of two
`NonUnitalSubring`s is typically not a `NonUnitalSubring`) -/
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubring 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 : NonUnitalSubring R :=
NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
(Subsemigroup.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⟩
