Closed initial segments as an open segment with a new top

noncomputable def ScottishBook155.initialSegmentToWithTop {J : Type u} [LinearOrder J] (j : J) : ↑(Set.Iic j) → WithTop ↑(Set.Iio j)

Map the endpoint of a closed initial segment to the added top element.

Equations

• ScottishBook155.initialSegmentToWithTop j x = if hx : ↑x < j then ↑⟨↑x, hx⟩ else ⊤

def ScottishBook155.initialSegmentFromWithTop {J : Type u} [LinearOrder J] (j : J) : WithTop ↑(Set.Iio j) → ↑(Set.Iic j)

Insert the added top element as the endpoint of the closed initial segment.

Equations

• ScottishBook155.initialSegmentFromWithTop j x = WithTop.recTopCoe ⟨j, ⋯⟩ (fun (i : ↑(Set.Iio j)) => ⟨↑i, ⋯⟩) x

noncomputable def ScottishBook155.initialSegmentWithTop {J : Type u} [LinearOrder J] (j : J) : ↑(Set.Iic j) ≃o WithTop ↑(Set.Iio j)

A closed initial segment is the corresponding open segment with one new top point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ScottishBook155.openSuccOrderIso {J : Type u} [LinearOrder J] [SuccOrder J] (j : J) (hj : ¬IsMax j) : ↑(Set.Iio (Order.succ j)) ≃o ↑(Set.Iic j)

The open segment below a successor is the closed segment below its predecessor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ScottishBook155.successorSegmentWithTop {J : Type u} [LinearOrder J] [SuccOrder J] (j : J) (hj : ¬IsMax j) : ↑(Set.Iic (Order.succ j)) ≃o WithTop ↑(Set.Iic j)

Decompose the closed segment at a successor into the previous closed segment and a new top.

Equations

• ScottishBook155.successorSegmentWithTop j hj = (ScottishBook155.initialSegmentWithTop (Order.succ j)).trans (ScottishBook155.openSuccOrderIso j hj).withTopCongr

@[simp]

theorem ScottishBook155.initialSegmentWithTop_apply_lt {J : Type u} [LinearOrder J] (j i : J) (hij : i < j) : (initialSegmentWithTop j) ⟨i, ⋯⟩ = ↑⟨i, hij⟩

@[simp]

theorem ScottishBook155.successorSegmentWithTop_apply_old {J : Type u} [LinearOrder J] [SuccOrder J] (j : J) (hj : ¬IsMax j) (i : ↑(Set.Iic j)) : (successorSegmentWithTop j hj) ⟨↑i, ⋯⟩ = ↑i