closure_iUnion

Mathlib.RingTheory.NonUnitalSubsemiring.Basic

URI: https://scilib.ai/kg/mathlib#NonUnitalSubsemiring.closure_iUnion

English

Closure commutes with indexed suprema: closure(⋃i s(i)) = ⨆ i, closure(s(i)).

Русский

Замыкание коммутирует с суммой по индексу: closure(⋃i s(i)) = ⨆i closure(s(i)).

LaTeX

$$$\\operatorname{closure}\\left(\\bigcup_i s(i)\\right) = \\bigvee_i \\operatorname{closure}(s(i))$$$

Lean4

theorem closure_iUnion {ι} (s : ι → Set R) : closure (⋃ i, s i) = ⨆ i, closure (s i) :=
  (NonUnitalSubsemiring.gi R).gc.l_iSup

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru