Theorems · Definition · logic and foundations

FirstOrder.Language.PartialEquiv.toEquiv

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → (self : L.PartialEquiv M N) → L.Equiv ↥self.dom ↥self.cod

The equivalence between the two subdomains.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

24 results in Mathlib

Foundations

Depth 18 from the axioms · uses no axioms

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure