coe_sSup_of_directedOn — Mathlib

English

The underlying set of the subsemiring iSup fun i => S i equals the union over i of the underlying sets of S i.

Русский

Множество iSup над directedOn равняется объединению всех соответствующих множеств S_i.

LaTeX

$$$\\text{coe}(\\iSup i, S_i) = \\bigcup_i \\text{coe}(S_i)$$$

Lean4

theorem coe_sSup_of_directedOn {S : Set (Subsemiring R)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S) :
    (↑(sSup S) : Set R) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Похожие утверждения