id_onBoundedFormula — Mathlib

English

The identity LHom on bounded formulas acts as the identity on each bounded formula.

Русский

Идентичность L-гомоморфизм на ограниченных формулах действует как единичный отображение на каждой ограниченной формуле.

LaTeX

$$$\\text{(LHom.id L).onBoundedFormula} = \\mathrm{id}$$$

Lean4

@[simp]
theorem id_onBoundedFormula : ((LHom.id L).onBoundedFormula : L.BoundedFormula α n → L.BoundedFormula α n) = id :=
  by
  ext f
  induction f with
  | falsum => rfl
  | equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
  | rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
  | imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
  | all _ ih3 => rw [onBoundedFormula, ih3, id, id]

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