Documentation

Mathlib.ModelTheory.LanguageMap

Language Maps #

Maps between first-order languages in the style of the Flypitch project, as well as several important maps between structures.

Main Definitions #

References #

For the Flypitch project:

structure FirstOrder.Language.LHom (L : FirstOrder.Language) (L' : FirstOrder.Language) :
Type (max (max (max u u') v) v')

A language homomorphism maps the symbols of one language to symbols of another.

  • onFunction : n : ⦄ → L.Functions nL'.Functions n
  • onRelation : n : ⦄ → L.Relations nL'.Relations n
Instances For

    A language homomorphism maps the symbols of one language to symbols of another.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def FirstOrder.Language.LHom.reduct {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
      L.Structure M

      Pulls a structure back along a language map.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem FirstOrder.Language.LHom.id_onRelation (L : FirstOrder.Language) (_n : ) (a : L.Relations _n) :
        (FirstOrder.Language.LHom.id L).onRelation a = id a
        @[simp]
        theorem FirstOrder.Language.LHom.id_onFunction (L : FirstOrder.Language) (_n : ) (a : L.Functions _n) :
        (FirstOrder.Language.LHom.id L).onFunction a = id a

        The identity language homomorphism.

        Equations
        Instances For
          Equations
          @[simp]
          theorem FirstOrder.Language.LHom.sumInl_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L.Functions _n) :
          FirstOrder.Language.LHom.sumInl.onFunction val = Sum.inl val
          @[simp]
          theorem FirstOrder.Language.LHom.sumInl_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L.Relations _n) :
          FirstOrder.Language.LHom.sumInl.onRelation val = Sum.inl val

          The inclusion of the left factor into the sum of two languages.

          Equations
          • FirstOrder.Language.LHom.sumInl = { onFunction := fun (_n : ) => Sum.inl, onRelation := fun (_n : ) => Sum.inl }
          Instances For
            @[simp]
            theorem FirstOrder.Language.LHom.sumInr_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L'.Relations _n) :
            FirstOrder.Language.LHom.sumInr.onRelation val = Sum.inr val
            @[simp]
            theorem FirstOrder.Language.LHom.sumInr_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (_n : ) (val : L'.Functions _n) :
            FirstOrder.Language.LHom.sumInr.onFunction val = Sum.inr val

            The inclusion of the right factor into the sum of two languages.

            Equations
            • FirstOrder.Language.LHom.sumInr = { onFunction := fun (_n : ) => Sum.inr, onRelation := fun (_n : ) => Sum.inr }
            Instances For
              @[simp]
              theorem FirstOrder.Language.LHom.ofIsEmpty_onFunction (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] {n : } (a : L.Functions n) :
              @[simp]
              theorem FirstOrder.Language.LHom.ofIsEmpty_onRelation (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] {n : } (a : L.Relations n) :
              def FirstOrder.Language.LHom.ofIsEmpty (L : FirstOrder.Language) (L' : FirstOrder.Language) [L.IsAlgebraic] [L.IsRelational] :
              L →ᴸ L'

              The inclusion of an empty language into any other language.

              Equations
              Instances For
                theorem FirstOrder.Language.LHom.funext_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} {F : L →ᴸ L'} {G : L →ᴸ L'} :
                F = G F.onFunction = G.onFunction F.onRelation = G.onRelation
                theorem FirstOrder.Language.LHom.funext {L : FirstOrder.Language} {L' : FirstOrder.Language} {F : L →ᴸ L'} {G : L →ᴸ L'} (h_fun : F.onFunction = G.onFunction) (h_rel : F.onRelation = G.onRelation) :
                F = G
                Equations
                @[simp]
                theorem FirstOrder.Language.LHom.comp_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') (_n : ) (F : L.Functions _n) :
                (g.comp f).onFunction F = g.onFunction (f.onFunction F)
                @[simp]
                theorem FirstOrder.Language.LHom.comp_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') :
                ∀ (x : ) (R : L.Relations x), (g.comp f).onRelation R = g.onRelation (f.onRelation R)

                The composition of two language homomorphisms.

                Equations
                • g.comp f = { onFunction := fun (_n : ) (F : L.Functions _n) => g.onFunction (f.onFunction F), onRelation := fun (x : ) (R : L.Relations x) => g.onRelation (f.onRelation R) }
                Instances For
                  theorem FirstOrder.Language.LHom.comp_assoc {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} {L3 : FirstOrder.Language} (F : L'' →ᴸ L3) (G : L' →ᴸ L'') (H : L →ᴸ L') :
                  (F.comp G).comp H = F.comp (G.comp H)
                  @[simp]
                  theorem FirstOrder.Language.LHom.sumElim_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (_n : ) :
                  ∀ (a : L.Functions _n L''.Functions _n), (ϕ.sumElim ψ).onFunction a = Sum.elim (fun (f : L.Functions _n) => ϕ.onFunction f) (fun (f : L''.Functions _n) => ψ.onFunction f) a
                  @[simp]
                  theorem FirstOrder.Language.LHom.sumElim_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (_n : ) :
                  ∀ (a : L.Relations _n L''.Relations _n), (ϕ.sumElim ψ).onRelation a = Sum.elim (fun (f : L.Relations _n) => ϕ.onRelation f) (fun (f : L''.Relations _n) => ψ.onRelation f) a

                  A language map defined on two factors of a sum.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem FirstOrder.Language.LHom.sumElim_comp_inl {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') :
                    (ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInl = ϕ
                    theorem FirstOrder.Language.LHom.sumElim_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') :
                    (ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInr = ψ
                    theorem FirstOrder.Language.LHom.sumElim_inl_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} :
                    FirstOrder.Language.LHom.sumInl.sumElim FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.id (L.sum L')
                    theorem FirstOrder.Language.LHom.comp_sumElim {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') {L3 : FirstOrder.Language} (θ : L' →ᴸ L3) :
                    θ.comp (ϕ.sumElim ψ) = (θ.comp ϕ).sumElim (θ.comp ψ)
                    @[simp]
                    theorem FirstOrder.Language.LHom.sumMap_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ) :
                    ∀ (a : L.Functions _n L₁.Functions _n), (ϕ.sumMap ψ).onFunction a = Sum.map (fun (f : L.Functions _n) => ϕ.onFunction f) (fun (f : L₁.Functions _n) => ψ.onFunction f) a
                    @[simp]
                    theorem FirstOrder.Language.LHom.sumMap_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ) :
                    ∀ (a : L.Relations _n L₁.Relations _n), (ϕ.sumMap ψ).onRelation a = Sum.map (fun (f : L.Relations _n) => ϕ.onRelation f) (fun (f : L₁.Relations _n) => ψ.onRelation f) a
                    def FirstOrder.Language.LHom.sumMap {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
                    L.sum L₁ →ᴸ L'.sum L₂

                    The map between two sum-languages induced by maps on the two factors.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem FirstOrder.Language.LHom.sumMap_comp_inl {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
                      (ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.sumInl.comp ϕ
                      @[simp]
                      theorem FirstOrder.Language.LHom.sumMap_comp_inr {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) :
                      (ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.sumInr.comp ψ

                      A language homomorphism is injective when all the maps between symbol types are.

                      Instances For
                        theorem FirstOrder.Language.LHom.Injective.onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} (self : ϕ.Injective) {n : } :
                        Function.Injective fun (f : L.Functions n) => ϕ.onFunction f
                        theorem FirstOrder.Language.LHom.Injective.onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} (self : ϕ.Injective) {n : } :
                        Function.Injective fun (R : L.Relations n) => ϕ.onRelation R
                        noncomputable def FirstOrder.Language.LHom.defaultExpansion {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : 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 u_1) [Inhabited M] [L.Structure M] :
                        L'.Structure M

                        Pulls an L-structure along a language map ϕ : L →ᴸ L', and then expands it to an L'-structure arbitrarily.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          class FirstOrder.Language.LHom.IsExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L.Structure M] [L'.Structure M] :

                          A language homomorphism is an expansion on a structure if it commutes with the interpretation of all symbols on that structure.

                          Instances
                            theorem FirstOrder.Language.LHom.IsExpansionOn.map_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} :
                            ∀ {inst : L.Structure M} {inst_1 : L'.Structure M} [self : ϕ.IsExpansionOn M] {n : } (f : L.Functions n) (x : Fin nM), FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
                            theorem FirstOrder.Language.LHom.IsExpansionOn.map_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} :
                            ∀ {inst : L.Structure M} {inst_1 : L'.Structure M} [self : ϕ.IsExpansionOn M] {n : } (R : L.Relations n) (x : Fin nM), FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
                            @[simp]
                            theorem FirstOrder.Language.LHom.map_onFunction {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n : } (f : L.Functions n) (x : Fin nM) :
                            @[simp]
                            theorem FirstOrder.Language.LHom.map_onRelation {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {M : Type u_1} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n : } (R : L.Relations n) (x : Fin nM) :
                            instance FirstOrder.Language.LHom.id_isExpansionOn {L : FirstOrder.Language} (M : Type u_1) [L.Structure M] :
                            (FirstOrder.Language.LHom.id L).IsExpansionOn M
                            Equations
                            • =
                            instance FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] [L.IsAlgebraic] [L.IsRelational] :
                            (FirstOrder.Language.LHom.ofIsEmpty L L').IsExpansionOn M
                            Equations
                            • =
                            instance FirstOrder.Language.LHom.sumElim_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L') (M : Type u_1) [L.Structure M] [L'.Structure M] [L''.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] :
                            (ϕ.sumElim ψ).IsExpansionOn M
                            Equations
                            • =
                            instance FirstOrder.Language.LHom.sumMap_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (M : Type u_1) [L.Structure M] [L'.Structure M] [L₁.Structure M] [L₂.Structure M] [ϕ.IsExpansionOn M] [ψ.IsExpansionOn M] :
                            (ϕ.sumMap ψ).IsExpansionOn M
                            Equations
                            • =
                            instance FirstOrder.Language.LHom.sumInl_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
                            FirstOrder.Language.LHom.sumInl.IsExpansionOn M
                            Equations
                            • =
                            instance FirstOrder.Language.LHom.sumInr_isExpansionOn {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type u_1) [L.Structure M] [L'.Structure M] :
                            FirstOrder.Language.LHom.sumInr.IsExpansionOn M
                            Equations
                            • =
                            @[simp]
                            theorem FirstOrder.Language.LHom.funMap_sumInl {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] [(L.sum L').Structure M] [FirstOrder.Language.LHom.sumInl.IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
                            @[simp]
                            theorem FirstOrder.Language.LHom.funMap_sumInr {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] [(L'.sum L).Structure M] [FirstOrder.Language.LHom.sumInr.IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
                            theorem FirstOrder.Language.LHom.sumInl_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} :
                            FirstOrder.Language.LHom.sumInl.Injective
                            theorem FirstOrder.Language.LHom.sumInr_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} :
                            FirstOrder.Language.LHom.sumInr.Injective
                            @[instance 100]
                            instance FirstOrder.Language.LHom.isExpansionOn_reduct {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') (M : Type u_1) [L'.Structure M] :
                            ϕ.IsExpansionOn M
                            Equations
                            • =
                            theorem FirstOrder.Language.LHom.Injective.isExpansionOn_default {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : 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 u_1) [Inhabited M] [L.Structure M] :
                            ϕ.IsExpansionOn M
                            structure FirstOrder.Language.LEquiv (L : FirstOrder.Language) (L' : FirstOrder.Language) :
                            Type (max (max (max u_1 u_2) u_3) u_4)

                            A language equivalence maps the symbols of one language to symbols of another bijectively.

                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                The identity equivalence from a first-order language to itself.

                                Equations
                                Instances For
                                  Equations
                                  @[simp]
                                  theorem FirstOrder.Language.LEquiv.symm_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') :
                                  e.symm.toLHom = e.invLHom
                                  @[simp]
                                  theorem FirstOrder.Language.LEquiv.symm_invLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} (e : L ≃ᴸ L') :
                                  e.symm.invLHom = e.toLHom

                                  The inverse of an equivalence of first-order languages.

                                  Equations
                                  • e.symm = { toLHom := e.invLHom, invLHom := e.toLHom, left_inv := , right_inv := }
                                  Instances For
                                    @[simp]
                                    theorem FirstOrder.Language.LEquiv.trans_toLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
                                    (e.trans e').toLHom = e'.toLHom.comp e.toLHom
                                    @[simp]
                                    theorem FirstOrder.Language.LEquiv.trans_invLHom {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (e : L ≃ᴸ L') (e' : L' ≃ᴸ L'') :
                                    (e.trans e').invLHom = e.invLHom.comp e'.invLHom

                                    The composition of equivalences of first-order languages.

                                    Equations
                                    • e.trans e' = { toLHom := e'.toLHom.comp e.toLHom, invLHom := e.invLHom.comp e'.invLHom, left_inv := , right_inv := }
                                    Instances For

                                      The type of functions for a language consisting only of constant symbols.

                                      Equations
                                      Instances For

                                        A language with constants indexed by a type.

                                        Equations
                                        Instances For
                                          Equations
                                          • =
                                          def FirstOrder.Language.constantsOn.structure {M : Type w} {α : Type u'} (f : αM) :

                                          Gives a constantsOn α structure to a type by assigning each constant a value.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            A map between index types induces a map between constant languages.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem FirstOrder.Language.constantsOnMap_isExpansionOn {M : Type w} {α : Type u'} {β : Type v'} {f : αβ} {fα : αM} {fβ : βM} (h : f = ) :

                                              Extends a language with a constant for each element of a parameter set in M.

                                              Equations
                                              Instances For

                                                Extends a language with a constant for each element of a parameter set in M.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem FirstOrder.Language.lhomWithConstants_onFunction (L : FirstOrder.Language) (α : Type w') (_n : ) (val : L.Functions _n) :
                                                  (L.lhomWithConstants α).onFunction val = Sum.inl val
                                                  @[simp]
                                                  theorem FirstOrder.Language.lhomWithConstants_onRelation (L : FirstOrder.Language) (α : Type w') (_n : ) (val : L.Relations _n) :
                                                  (L.lhomWithConstants α).onRelation val = Sum.inl val
                                                  def FirstOrder.Language.lhomWithConstants (L : FirstOrder.Language) (α : Type w') :
                                                  L →ᴸ L.withConstants α

                                                  The language map adding constants.

                                                  Equations
                                                  • L.lhomWithConstants α = FirstOrder.Language.LHom.sumInl
                                                  Instances For
                                                    theorem FirstOrder.Language.lhomWithConstants_injective (L : FirstOrder.Language) (α : Type w') :
                                                    (L.lhomWithConstants α).Injective
                                                    def FirstOrder.Language.con (L : FirstOrder.Language) {α : Type w'} (a : α) :
                                                    (L.withConstants α).Constants

                                                    The constant symbol indexed by a particular element.

                                                    Equations
                                                    Instances For
                                                      def FirstOrder.Language.LHom.addConstants {L : FirstOrder.Language} (α : Type w') {L' : FirstOrder.Language} (φ : L →ᴸ L') :
                                                      L.withConstants α →ᴸ L'.withConstants α

                                                      Adds constants to a language map.

                                                      Equations
                                                      Instances For
                                                        def FirstOrder.Language.LEquiv.addEmptyConstants (L : FirstOrder.Language) (α : Type w') [ie : IsEmpty α] :
                                                        L ≃ᴸ L.withConstants α

                                                        The language map removing an empty constant set.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem FirstOrder.Language.withConstants_funMap_sum_inl (L : FirstOrder.Language) {M : Type w} [L.Structure M] {α : Type w'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {f : L.Functions n} {x : Fin nM} :
                                                          @[simp]
                                                          theorem FirstOrder.Language.withConstants_relMap_sum_inl (L : FirstOrder.Language) {M : Type w} [L.Structure M] {α : Type w'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {R : L.Relations n} {x : Fin nM} :
                                                          def FirstOrder.Language.lhomWithConstantsMap (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} (f : αβ) :
                                                          L.withConstants α →ᴸ L.withConstants β

                                                          The language map extending the constant set.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem FirstOrder.Language.LHom.map_constants_comp_sumInl (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} {f : αβ} :
                                                            (L.lhomWithConstantsMap f).comp FirstOrder.Language.LHom.sumInl = L.lhomWithConstants β
                                                            Equations
                                                            instance FirstOrder.Language.withConstantsSelfStructure (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
                                                            (L.withConstants M).Structure M
                                                            Equations
                                                            instance FirstOrder.Language.withConstants_self_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
                                                            (L.lhomWithConstants M).IsExpansionOn M
                                                            Equations
                                                            • =
                                                            instance FirstOrder.Language.withConstantsStructure (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] :
                                                            (L.withConstants α).Structure M
                                                            Equations
                                                            instance FirstOrder.Language.withConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] :
                                                            (L.lhomWithConstants α).IsExpansionOn M
                                                            Equations
                                                            • =
                                                            Equations
                                                            • =
                                                            Equations
                                                            • =
                                                            instance FirstOrder.Language.addConstants_expansion (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] {L' : FirstOrder.Language} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] :
                                                            Equations
                                                            • =
                                                            @[simp]
                                                            theorem FirstOrder.Language.withConstants_funMap_sum_inr (L : FirstOrder.Language) {M : Type w} [L.Structure M] (α : Type u_1) [(FirstOrder.Language.constantsOn α).Structure M] {a : α} {x : Fin 0M} :
                                                            @[simp]
                                                            theorem FirstOrder.Language.coe_con (L : FirstOrder.Language) {M : Type w} [L.Structure M] (A : Set M) {a : A} :
                                                            (L.con a) = a
                                                            Equations
                                                            • =
                                                            instance FirstOrder.Language.map_constants_inclusion_isExpansionOn (L : FirstOrder.Language) {M : Type w} [L.Structure M] {A : Set M} {B : Set M} (h : A B) :
                                                            (L.lhomWithConstantsMap (Set.inclusion h)).IsExpansionOn M
                                                            Equations
                                                            • =