Intervals as initial segments

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

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

Iic j is an initial segment.

Equations

• Set.initialSegIic j = { toFun := fun (j_1 : ↑(Set.Iic j)) => ↑j_1, inj' := ⋯, map_rel_iff' := ⋯, mem_range_of_rel' := ⋯ }

@[simp]

theorem Set.initialSegIic_toFun {α : Type u_1} [Preorder α] (j : α) (j✝ : ↑(Iic j)) : (initialSegIic j) j✝ = ↑j✝

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

Iio j is a principal segment.

Equations

• Set.principalSegIio j = { toFun := fun (j_1 : ↑(Set.Iio j)) => ↑j_1, inj' := ⋯, map_rel_iff' := ⋯, top := j, mem_range_iff_rel' := ⋯ }

@[simp]

theorem Set.principalSegIio_toFun {α : Type u_1} [Preorder α] (j : α) (j✝ : ↑(Iio j)) : (principalSegIio j).toFun j✝ = ↑j✝

@[simp]

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

@[simp]

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

@[deprecated Set.principalSegIio_apply (since := "2026-04-12")]

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

Alias of Set.principalSegIio_apply.

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 Iic i is an initial segment of Iic j.

Equations

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

@[simp]

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

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 Iio i is a principal segment of Iic j.

Equations

• Set.principalSegIioIicOfLE h = { toFun := fun (k : ↑(Set.Iio i)) => ⟨↑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_apply {α : Type u_1} [Preorder α] {i j : α} (h : i ≤ j) (k : ↑(Iio i)) : (principalSegIioIicOfLE h).toRelEmbedding k = ⟨↑k, ⋯⟩

@[deprecated Set.principalSegIioIicOfLE_apply (since := "2026-04-12")]

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

Alias of Set.principalSegIioIicOfLE_apply.

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 Iio f.top.

Equations

• f.orderIsoIio = OrderIso.ofRelIsoLT f.subrelIso.symm

@[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✝