Theorems · Definition · logic and foundations

FirstOrder.Language.LEquiv.mk.noConfusion

{L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    {P : Sort u} →
      {toLHom : L →ᴸ L'} →
        {invLHom : L' →ᴸ L} →
          {left_inv : invLHom.comp toLHom = FirstOrder.Language.LHom.id L} →
            {right_inv : toLHom.comp invLHom = FirstOrder.Language.LHom.id L'} →
              {toLHom' : L →ᴸ L'} →
                {invLHom' : L' →ᴸ L} →
                  {left_inv' : invLHom'.comp toLHom' = FirstOrder.Language.LHom.id L} →
                    {right_inv' : toLHom'.comp invLHom' = FirstOrder.Language.LHom.id L'} →
                      { toLHom := toLHom, invLHom := invLHom, left_inv := left_inv, right_inv := right_inv } =
                          { toLHom := toLHom', invLHom := invLHom', left_inv := left_inv', right_inv := right_inv' } →
                        (toLHom ≍ toLHom' → invLHom ≍ invLHom' → P) → P

Defined in

Mathlib.ModelTheory.LanguageMap

Cited by

1 results in Mathlib

Foundations

Depth 23 from the axioms · uses no axioms