coe_iSup_of_directed — Mathlib

English

If ι is nonempty and (K_i) is a directed family of Subalgebras, the carrier of iSup K is the union of the carriers of K_i.

Русский

Если индекс множество непусто и (K_i) — направленная семейство Subalgebra, то карриер iSup K равен объединению карриеров K_i.

LaTeX

$$$\uparrow(\mathrm{iSup}\,K) = \bigcup_{i} (K_i : Set A)$$$

Lean4

theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃ i, (K i : Set A) :=
  let s : Subalgebra R A :=
    { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
      algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2 ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
  have : iSup K = s :=
    le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
  this.symm ▸ rfl

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