English
Let (l_i) be a family of languages indexed by i in a nonempty index set ι, and let m be a language. Then the supremum of the family, added with m on the right, equals the supremum of the family with m added to each term: (⋁_i l_i) + m = ⋁_i (l_i + m).
Русский
Пусть (L_i) — семейство языков, индексируемое по i из непустого множества ι, и пусть m — язык. Тогда суммарная верхняя граница семейства, прибавленная справа к m, равна верхней границе всех членов, к каждому из которых добавлен m: (⋁_i L_i) + m = ⋁_i (L_i + m).
LaTeX
$$$\\left( \\bigvee_{i} l(i) \\right) + m = \\bigvee_{i} (l(i) + m)$$$
Lean4
theorem iSup_add {ι : Sort v} [Nonempty ι] (l : ι → Language α) (m : Language α) : (⨆ i, l i) + m = ⨆ i, l i + m :=
iSup_sup
