defaultExpansion — Mathlib

Lean4
/-- Pulls an `L`-structure along a language map `ϕ : L →ᴸ L'`, and then expands it
  to an `L'`-structure arbitrarily. -/
noncomputable def defaultExpansion (ϕ : 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)] (M : Type*)
    [Inhabited M] [L.Structure M] : L'.Structure M
    where
  funMap {n} f xs := if h' : f ∈ Set.range fun f : L.Functions n => onFunction ϕ f then funMap h'.choose xs else default
  RelMap {n} r xs := if h' : r ∈ Set.range fun r : L.Relations n => onRelation ϕ r then RelMap h'.choose xs else default
Похожие утверждения