castLE_comp_castLE — Mathlib

English

The composition of castings equals a single cast: Function composition of castLE maps equals castLE via composition law.

Русский

Составление приведения равно единичному приведения через составление функций.

LaTeX

$$$\forall {L} {\alpha} {k m n} (km : k \le m) (mn : m \le n),\; (BoundedFormula.castLE mn \circ BoundedFormula.castLE km) = BoundedFormula.castLE (km.trans mn).$$$

Lean4

@[simp]
theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
    (BoundedFormula.castLE mn ∘ BoundedFormula.castLE km : L.BoundedFormula α k → L.BoundedFormula α n) =
      BoundedFormula.castLE (km.trans mn) :=
  funext (castLE_castLE km mn)

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