iSup_toSubsemiring — Mathlib

English

For a nonempty index set, the iSup of a family of Subalgebras maps to the iSup of their Subsemirings: (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring.

Русский

Для непустого индекса: iSup S отображается в iSup подпсемирингов: (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring.

LaTeX

$$$\left(\bigvee_i S_i\right).toSubsemiring = \bigvee_i \left(S_i.toSubsemiring\right)$$$

Lean4

@[simp]
theorem iSup_toSubsemiring {ι : Sort*} [Nonempty ι] (S : ι → Subalgebra R A) :
    (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring := by
  simp only [iSup, Set.range_nonempty, sSup_toSubsemiring, ← Set.range_comp, Function.comp_def]

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