castLE_castLE — Mathlib

English

Casting twice composes to casting once: (castLE km).castLE mn = castLE (km ∘ mn).

Русский

Дваждые приведения индексов compose стабильно: castLE km затем castLE mn равно castLE (km ∘ mn).

LaTeX

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

Lean4

@[simp]
theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (φ : L.BoundedFormula α k) :
    (φ.castLE km).castLE mn = φ.castLE (km.trans mn) :=
  by
  revert m n
  induction φ with
  | falsum => intros; rfl
  | equal => simp
  | rel =>
    intros
    simp only [castLE]
    rw [← Function.comp_assoc, Term.relabel_comp_relabel]
    simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => intros; simp only [castLE, ih3]

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