mapTermRel_id_id_id — Mathlib

English

Mapping with identity transformations leaves the formula unchanged.

Русский

Сопоставление через тождественные отображения не изменяет формулу.

LaTeX

$$$\forall φ,\; \mathrm{mapTermRel} (id) (id) (id) (φ) = φ$.$$

Lean4

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

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