Theorems · Definition · logic and foundations

FirstOrder.Language.StrongHomClass.toEquiv

{L : FirstOrder.Language} →
  {F : Type u_3} →
    {M : Type u_4} →
      {N : Type u_5} →
        [inst : L.Structure M] →
          [inst_1 : L.Structure N] → [inst_2 : EquivLike F M N] → [L.StrongHomClass F M N] → F → L.Equiv M N

Any element of a bijective StrongHomClass can be realized as a first order isomorphism.

Defined in

Mathlib.ModelTheory.Basic

Cited by

4 results in Mathlib

Foundations

Depth 10 from the axioms · uses Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureEquivLikeFirstOrder.Language.StrongHomClass