iSup_mul

Mathlib.Computability.Language

URI: https://scilib.ai/kg/mathlib#Language.iSup_mul

English

The iSup of languages distributes over multiplication: (⨆ i, l i) * m = ⨆ i, l i * m.

Русский

Пусть iSup языков распределяется по умножению: (⨆ i, l i) * m = ⨆ i, l i * m.

LaTeX

$$$ (\bigsqcup_i l_i) * m = \bigsqcup_i (l_i * m) $$$

Lean4

theorem iSup_mul {ι : Sort v} (l : ι → Language α) (m : Language α) : (⨆ i, l i) * m = ⨆ i, l i * m :=
  image2_iUnion_left _ _ _

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

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

Разделы

Аффилиация

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