Theorems · Definition · order theory

Order.PartialIso.definedAtLeft

{α : Type u_1} →
  (β : Type u_2) →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] →
        [DenselyOrdered β] → [NoMinOrder β] → [NoMaxOrder β] → [Nonempty β] → α → Order.Cofinal (Order.PartialIso α β)

The set of partial isomorphisms defined at a : α, together with a proof that any partial isomorphism can be extended to one defined at a.

Defined in

Mathlib.Order.CountableDenseLinearOrder

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderLinearOrderDenselyOrderedNoMinOrderNoMaxOrderNonempty