English
Two successive mapTermRel operations commute up to natural reindexing; applying a second mapTermRel to the result equals applying a composed map to the original formula.
Русский
Две последовательные операции mapTermRel коммутируют до естественной индексации; применение второй mapTermRel к результату равно применению композиции отображений к исходной формуле.
LaTeX
$$$((\varphi.mapTermRel ft fr id).mapTermRel ft' fr' id) = (\varphi.mapTermRel (ft' \circ ft) (fr' \circ fr) id).$$$
Lean4
@[simp]
theorem mapTermRel_mapTermRel {L'' : Language} (ft : ∀ n, L.Term (α ⊕ (Fin n)) → L'.Term (β ⊕ (Fin n)))
(fr : ∀ n, L.Relations n → L'.Relations n) (ft' : ∀ n, L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ (Fin n)))
(fr' : ∀ n, L'.Relations n → L''.Relations n) {n} (φ : L.BoundedFormula α n) :
((φ.mapTermRel ft fr fun _ => id).mapTermRel ft' fr' fun _ => id) =
φ.mapTermRel (fun _ => ft' _ ∘ ft _) (fun _ => fr' _ ∘ fr _) 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]
