English
Let {S_i} be a directed family of nonunital subsemirings of a nonunital semiring R. For every x in R, x belongs to the supremum ⨆ i, S_i if and only if there exists an index i with x ∈ S_i.
Русский
Пусть {S_i} — направленная семейство неединичных подпsemiring R. Для каждого x ∈ R верно: x ∈ ⨆ i, S_i тогда и только тогда, когда существует индекс i, такой что x ∈ S_i.
LaTeX
$$$ (x \in \bigsqcup_i S_i) \leftrightarrow \exists i, x \in S_i $$$
Lean4
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → NonUnitalSubsemiring 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 : NonUnitalSubsemiring R :=
NonUnitalSubsemiring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (Subsemigroup.coe_iSup_of_directed hS)
(⨆ i, (S i).toAddSubmonoid) (AddSubmonoid.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⟩
