English
If ϕ is an expansion, then map_onRelation respects onRelation with RelMap.
Русский
Если ϕ — расширение, то map_onRelation согласуется с RelMap.
LaTeX
$$$RelMap(\varphi.onRelation R)\, x = RelMap R\, x$$$
Lean4
theorem isExpansionOn_default {ϕ : L →ᴸ L'}
[∀ (n) (f : L'.Functions n), Decidable (f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f)]
[∀ (n) (r : L'.Relations n), Decidable (r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r)] (h : ϕ.Injective)
(M : Type*) [Inhabited M] [L.Structure M] : @IsExpansionOn L L' ϕ M _ (ϕ.defaultExpansion M) :=
by
letI := ϕ.defaultExpansion M
refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
· have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
refine (dif_pos hf).trans ?_
rw [h.onFunction hf.choose_spec]
· have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
refine (dif_pos hr).trans ?_
rw [h.onRelation hr.choose_spec]
