Theorems · Definition · logic and foundations

FirstOrder.Language.PartialEquiv.toEmbedding

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

A partial equivalence as an embedding from its domain.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure