Appending a protected successor to a coherent chain

This file packages the successor clause independently of the transfinite recursion. The new index is the top point of WithTop ι.

noncomputable def ScottishBook155.ProtectedChain.link {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) (i j : ι) (hij : i ≤ j) : ProtectedLink (C.stage i) (C.stage j) L

The coherent systems of a chain give a protected link between any two comparable stages.

Equations

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

noncomputable def ScottishBook155.ProtectedChain.appendStage {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) : WithTop ι → ProtectedStage r

The stage family obtained by adjoining a new top stage.

Equations

• ScottishBook155.ProtectedChain.appendStage T none = T.next
• ScottishBook155.ProtectedChain.appendStage T (some i) = C.stage i

noncomputable def ScottishBook155.ProtectedChain.appendLink {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) (i j : WithTop ι) (hij : i ≤ j) : ProtectedLink (appendStage T i) (appendStage T j) L

Links in the chain with one new top stage.

Equations

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

@[simp]

theorem ScottishBook155.ProtectedChain.appendLink_coe_coe {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) (i j : ι) (hij : ↑i ≤ ↑j) : appendLink T (↑i) (↑j) hij = C.link i j ⋯

@[simp]

theorem ScottishBook155.ProtectedChain.appendLink_coe_top {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) (i : ι) : appendLink T ↑i ⊤ ⋯ = (C.link i ⊤ ⋯).extend T

@[simp]

theorem ScottishBook155.ProtectedChain.appendLink_top_top {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) : appendLink T ⊤ ⊤ ⋯ = ProtectedLink.refl T.next

noncomputable def ScottishBook155.ProtectedChain.append {ι : Type u} [LinearOrder ι] [OrderTop ι] {r L : ℝ} {C : ProtectedChain r L} (T : ProtectedTransition (C.stage ⊤) L) : ProtectedChain r L

The coherent protected chain after one successor transition.

Equations

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

theorem ScottishBook155.ProtectedChain.append_reindex_withTopCoe {κ : Type} [LinearOrder κ] [OrderTop κ] {r L : ℝ} (D : ProtectedChain r L) (T : ProtectedTransition (D.stage ⊤) L) : (append T).reindex withTopCoeOrderEmbedding = D

Restricting an appended successor chain back to the old indices recovers the original chain.