Theorems · Theorem · logic and foundations

FirstOrder.Language.Equiv.comp_toEmbedding

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N),
  (hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding

Defined in

Mathlib.ModelTheory.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFirstOrder.Language.Structure