add_iSup — Mathlib

English

Let (l_i) be a family of languages indexed by i in a nonempty ι, and let m be a language. Then left-addition distributes over iSup: (m + ⋁_i l_i) = ⋁_i (m + l_i).

Русский

Пусть (L_i) — семейство языков, индексируемое по i из непустого множества ι, и пусть m — язык. Тогда сложение слева распределяет над iSup: m + ⋁_i L_i = ⋁_i (m + L_i).

LaTeX

$$$m + \\bigvee_{i} l(i) = \\bigvee_{i} (m + l(i))$$$

Lean4

theorem add_iSup {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : (m + ⨆ i, l i) = ⨆ i, m + l i :=
  sup_iSup

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