Theorems · Definition · logic and foundations

FirstOrder.Language.Embedding.equivRange

{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → (f : L.Embedding M N) → L.Equiv M ↥f.toHom.range

The equivalence between the domain and the range of an embedding f.

Defined in

Mathlib.ModelTheory.Substructures

Cited by

14 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure