Theorems · Definition · logic and foundations

FirstOrder.Language.DirectLimit.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 ι] → [Nonempty ι] → [IsDirectedOrder ι] → (ι →o L.PartialEquiv M N) → L.PartialEquiv M N

The limit of a directed system of PartialEquivs.

Defined in

Mathlib.ModelTheory.PartialEquiv

Cited by

6 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructurePreorderNonemptyIsDirectedOrder