Theorems · Definition · order theory

Order.PartialIso.definedAtRight

(α : 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 b : β, together with a proof that any partial isomorphism can be extended to include b. We prove this by symmetry.

Defined in

Mathlib.Order.CountableDenseLinearOrder

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderLinearOrderDenselyOrderedNoMinOrderNoMaxOrderNonempty