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.

@[implicit_reducible]

def Set.initialSegIic {α : Type u_1} [Preorder α] (j : α) : ↑(Iic j) ≤i α

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✝

@[implicit_reducible]

def Set.principalSegIio {α : Type u_1} [Preorder α] (j : α) : ↑(Iio j) <i α

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

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

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) : ↑(Iio i) <i ↑(Iic j)

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, ⋯⟩

noncomputable def PrincipalSeg.orderIsoIio {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : α <i β) : α ≃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 : α <i β) (a✝ : α) : ↑(f.orderIsoIio a✝) = f.toRelEmbedding a✝