Occurrence calculus for language maps

The exact image laws for LHom.onTerm / BoundedFormulaω.mapLanguage: symbol occurrences of a mapped object are the image of the original's occurrences under the symbol map.

Neutral by construction — no schema, interpolation or PC content. These were previously duplicated across SchemaCompletion.lean, Interpolation/CraigRelational.lean and LopezEscobar/PCSentence.lean; the last two declared the same name BoundedFormulaω.relationsIn_mapLanguage, so which one a downstream file saw depended on import order. Consolidating here removes that hazard.

theorem FirstOrder.Language.Term.functionsIn_onTerm {L L' : Language} (g : L →ᴸ L') {α : Type} (t : L.Term α) : (g.onTerm t).functionsIn = (fun (p : (n : ℕ) × L.Functions n) => ⟨p.fst, g.onFunction p.snd⟩) '' t.functionsIn

functionsIn of a language-mapped term is the image of the term's functionsIn under the symbol map ⟨n, f⟩ ↦ ⟨n, g.onFunction f⟩.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_mapLanguage {L L' : Language} (g : L →ᴸ L') {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : (mapLanguage g φ).functionsIn = (fun (p : (n : ℕ) × L.Functions n) => ⟨p.fst, g.onFunction p.snd⟩) '' φ.functionsIn

functionsIn of a language-mapped formula is the image of the formula's functionsIn under the symbol map ⟨n, f⟩ ↦ ⟨n, g.onFunction f⟩.

relationsIn of a language-mapped formula (companion to functionsIn_mapLanguage)

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_mapLanguage {L L' : Language} (g : L →ᴸ L') {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : (mapLanguage g φ).relationsIn = (fun (p : (n : ℕ) × L.Relations n) => ⟨p.fst, g.onRelation p.snd⟩) '' φ.relationsIn