mul_iSup

Mathlib.Computability.Language

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

English

Multiplication distributes on the left over iSup: m * (⨆ i, l i) = ⨆ i, m * l i.

Русский

Деление слева распространяется на iSup: m * (⨆ i, l i) = ⨆ i, m * l i.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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