Intervals as initial segments

We show that Set.Iic and Set.Iio are respectively initial and principal segments, and that any principal segment f is order isomorphic to Set.Iio f.top.

def Set.initialSegIic {α : Type u_1} [Preorder α] (j : α) : InitialSeg (fun (x1 x2 : ↑(Iic j)) => x1 < x2) fun (x1 x2 : α) => x1 < x2

Set.Iic j is an initial segment.

Equations

• Set.initialSegIic j = { toFun := fun (x : ↑(Set.Iic j)) => match x with | ⟨j_1, hj⟩ => j_1, inj' := ⋯, map_rel_iff' := ⋯, mem_range_of_rel' := ⋯ }

@[simp]

theorem Set.initialSegIic_toFun {α : Type u_1} [Preorder α] (j : α) (x✝ : ↑(Iic j)) : (initialSegIic j) x✝ = match x✝ with | ⟨j_1, hj⟩ => j_1

def Set.principalSegIio {α : Type u_1} [Preorder α] (j : α) : PrincipalSeg (fun (x1 x2 : ↑(Iio j)) => x1 < x2) fun (x1 x2 : α) => x1 < x2

Set.Iio j is a principal segment.

Equations

• Set.principalSegIio j = { toFun := fun (x : ↑(Set.Iio j)) => match x with | ⟨j_1, hj⟩ => j_1, inj' := ⋯, map_rel_iff' := ⋯, top := j, mem_range_iff_rel' := ⋯ }

@[simp]

theorem Set.principalSegIio_toFun {α : Type u_1} [Preorder α] (j : α) (x✝ : ↑(Iio j)) : (principalSegIio j).toFun x✝ = match x✝ with | ⟨j_1, hj⟩ => j_1

@[simp]

theorem Set.principalSegIio_top {α : Type u_1} [Preorder α] (j : α) : (principalSegIio j).top = j

@[simp]

theorem Set.principalSegIio_toRelEmbedding {α : Type u_1} [Preorder α] {j : α} (k : ↑(Iio j)) : (principalSegIio j).toRelEmbedding k = ↑k

def Set.initialSegIicIicOfLE {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) : InitialSeg (fun (x1 x2 : ↑(Iic i)) => x1 < x2) fun (x1 x2 : ↑(Iic j)) => x1 < x2

If i ≤ j, then Set.Iic i is an initial segment of Set.Iic j.

Equations

• Set.initialSegIicIicOfLE h = { toFun := fun (x : ↑(Set.Iic i)) => match x with | ⟨k, hk⟩ => ⟨k, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯, mem_range_of_rel' := ⋯ }

@[simp]

theorem Set.initialSegIicIicOfLE_toFun_coe {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) (x✝ : ↑(Iic i)) : ↑((initialSegIicIicOfLE h) x✝) = ↑x✝

def Set.principalSegIioIicOfLE {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) : PrincipalSeg (fun (x1 x2 : ↑(Iio i)) => x1 < x2) fun (x1 x2 : ↑(Iic j)) => x1 < x2

If i ≤ j, then Set.Iio i is a principal segment of Set.Iic j.

Equations

• Set.principalSegIioIicOfLE h = { toFun := fun (x : ↑(Set.Iio i)) => match x with | ⟨k, hk⟩ => ⟨k, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯, top := ⟨i, h⟩, mem_range_iff_rel' := ⋯ }

@[simp]

theorem Set.principalSegIioIicOfLE_top {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) : (principalSegIioIicOfLE h).top = ⟨i, h⟩

@[simp]

theorem Set.principalSegIioIicOfLE_toRelEmbedding {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) (k : ↑(Iio i)) : (principalSegIioIicOfLE h).toRelEmbedding k = ⟨↑k, ⋯⟩

noncomputable def PrincipalSeg.orderIsoIio {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) : α ≃o ↑(Set.Iio f.top)

If f : α <i β is a principal segment, this is the induced order isomorphism α ≃o Set.Iio f.top.

Equations

• f.orderIsoIio = { toEquiv := Equiv.ofBijective (fun (a : α) => ⟨f.toRelEmbedding a, ⋯⟩) ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem PrincipalSeg.orderIsoIio_apply_coe {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) (a : α) : ↑(f.orderIsoIio a) = f.toRelEmbedding a