theorem
WellOrder.either_embeds
(α : Type u_3)
(β : Type u_4)
[WellOrder α]
[WellOrder β]
:
(∃ (x : WellOrder.InitialSegment β), ∃ (f : α → ↥x.val), IsOrderIso f) ∨ ∃ (x : WellOrder.InitialSegment α), ∃ (f : ↥x.val → β), IsOrderIso f
theorem
WellOrder.segment_less_strictly_monotone
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{f g : α → β}
(hdc : (f '' Set.univ).IsDownwardsClosed)
(hf : Monotone f)
(hg : StrictMonotone g)
{x : α}
:
f x ≤ g x
theorem
WellOrder.segment_embedding_all_eq'
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{x y : WellOrder.InitialSegment α}
{f : ↥x.val → β}
{g : ↥y.val → β}
(hs : x.val ⊆ y.val)
(hf : IsOrderIso f)
(hg : IsOrderIso g)
:
∃ (h : x = y), Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment α) (h : x = x_1) => ↥x_1.val → β) f h = g
theorem
WellOrder.segment_embedding_all_eq
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{x y : WellOrder.InitialSegment α}
{f : ↥x.val → β}
{g : ↥y.val → β}
(hf : IsOrderIso f)
(hg : IsOrderIso g)
:
∃ (h : x = y), Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment α) (h : x = x_1) => ↥x_1.val → β) f h = g
theorem
WellOrder.into_segment_embedding_all_eq'
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{x y : WellOrder.InitialSegment β}
{f : α → ↥x.val}
{g : α → ↥y.val}
(hs : x.val ⊆ y.val)
(hf : IsOrderIso f)
(hg : IsOrderIso g)
:
∃ (h : x = y), Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment β) (h : x = x_1) => α → ↥x_1.val) f h = g
theorem
WellOrder.into_segment_embedding_all_eq
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{x y : WellOrder.InitialSegment β}
{f : α → ↥x.val}
{g : α → ↥y.val}
(hf : IsOrderIso f)
(hg : IsOrderIso g)
:
∃ (h : x = y), Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment β) (h : x = x_1) => α → ↥x_1.val) f h = g
theorem
WellOrder.segment_into_self_iso
{α : Type u_1}
[WellOrder α]
{x : WellOrder.InitialSegment α}
{f : ↥x.val → α}
(h : IsOrderIso f)
:
∃ (h : x = WellOrder.InitialSegment.univ),
Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment α) (h : x = x_1) => ↥x_1.val → α) f h = Subtype.val
theorem
WellOrder.self_into_segment_iso
{α : Type u_1}
[WellOrder α]
{x : WellOrder.InitialSegment α}
{f : α → ↥x.val}
(h : IsOrderIso f)
:
∃ (h : x = WellOrder.InitialSegment.univ),
Eq.rec (motive := fun (x_1 : WellOrder.InitialSegment α) (h : x = x_1) => α → ↥x_1.val) f h = fun (x : α) =>
⟨x, True.intro⟩
theorem
WellOrder.iso_all_eq
{α : Type u_1}
{β : Type u_2}
[WellOrder α]
[WellOrder β]
{f g : α → β}
(hf : IsOrderIso f)
(hg : IsOrderIso g)
:
f = g
theorem
WellOrder.iso_same_eq_id
{α : Type u_1}
[WellOrder α]
{f : α → α}
(h : IsOrderIso f)
:
f = id
theorem
WellOrder.subset_iso_segment
{α : Type u_1}
[WellOrder α]
{s : Set α}
:
∃ (t : WellOrder.InitialSegment α), ∃ (f : ↥s → ↥t.val), IsOrderIso f