coe_sSup_of_directedOn — Mathlib

English

Let S be a directed, nonempty set of subfields of K. Then the carrier of sSup S equals the union of carriers of elements of S.

Русский

Пусть S — направленное непустое множество подполей K. Тогда носитель sSup S равен объединению носителей элементов S.

LaTeX

$$$\uparrow(\operatorname{sSup} S) = \bigcup_{s \in S} \uparrow s$$$

Lean4

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

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