Theorems · Theorem · logic and foundations

FirstOrder.Language.DirectLimit.cod_partialEquivLimit

∀ {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),
  (FirstOrder.Language.DirectLimit.partialEquivLimit S).cod = ⨆ x, (S x).cod

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructurePreorderNonemptyIsDirectedOrder