Theorems · Definition · logic and foundations

FirstOrder.Language.PartialEquiv.toEquivOfEqTop

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → {f : L.PartialEquiv M N} → f.dom = ⊤ → f.cod = ⊤ → L.Equiv M N

Given a partial equivalence which has the whole structure as domain and as codomain, returns the corresponding equivalence.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

2 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure