reverse_iInf — Mathlib

English

Reversing the infimum of a family equals the infimum of the reverses: (∧_i l_i).reverse = ∧_i (l_i.reverse).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem reverse_iInf {ι : Sort*} (l : ι → Language α) : (⨅ i, l i).reverse = ⨅ i, (l i).reverse :=
  preimage_iInter

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