reverse_iSup — Mathlib

English

Reversing the supremum of a family equals the supremum of the reverses: (⋁_i l_i).reverse = ⋁_i (l_i.reverse).

Русский

Разворот наибольшей верхней границы семейства равен верхней границе разворотов членов: (⋁_i l_i).reverse = ⋁_i (l_i.reverse).

LaTeX

$$$\\left( \\bigvee_{i} l_i \\right)^{\\text{reverse}} = \\bigvee_{i} (l_i^{\\text{reverse}})$$$

Lean4

@[simp]
theorem reverse_iSup {ι : Sort*} (l : ι → Language α) : (⨆ i, l i).reverse = ⨆ i, (l i).reverse :=
  preimage_iUnion

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