castLE_rfl — Mathlib

English

Casting along a reflexive bound is the identity: castLE with h: n ≤ n leaves formulas unchanged.

Русский

Пере castLE по тождественному неравенству не изменяет формулу.

LaTeX

$$$\forall n (h : n \le n) (\varphi : L.BoundedFormula α n),\; \mathrm{castLE}(h, \varphi) = \varphi.$$$

Lean4

@[simp]
theorem castLE_rfl {n} (h : n ≤ n) (φ : L.BoundedFormula α n) : φ.castLE h = φ := by
  induction φ with
  | falsum => rfl
  | equal => simp
  | rel => simp
  | imp _ _ ih1 ih2 => simp [ih1, ih2]
  | all _ ih3 => simp [ih3]

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