coe_iSup_of_directed — Mathlib

English

Let S be a nonempty set of subfields of K directed by inclusion. Then the underlying set of the iSup equals the union of the underlying sets: ((iSup i, S i) : Set K) = ⋃ i, ↑(S i).

Русский

Пусть S — непустой набор подполей K, направленный по включению. Тогда каркас iSup равен объединению каркасов: ((iSup i, S i) : Set K) = ⋃ i, ↑(S i).

LaTeX

$$$((\iSup i, S i : Subfield K) : \text{Set } K) = \bigcup_{i} \uparrow (S i)$$$

Lean4

theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subfield K) : Set K) = ⋃ i, ↑(S i) :=
  Set.ext fun x => by simp [mem_iSup_of_directed hS]

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