Theorems · Theorem · logic and foundations

FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion

∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {ι : Type u_1}
  [inst_2 : Preorder ι] [inst_3 : Nonempty ι] [inst_4 : IsDirectedOrder ι] (S : ι →o L.PartialEquiv M N) {i : ι},
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).toEquiv.toEmbedding.comp
      (FirstOrder.Language.Substructure.inclusion ⋯) =
    (FirstOrder.Language.Substructure.inclusion ⋯).comp (S i).toEquiv.toEmbedding

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructurePreorderNonemptyIsDirectedOrder