The active-or-idle scheduled successor

At a scheduled transition the named target point is either already hit, in which case the transition is idle, or it is added by the protected one-point extension.

noncomputable def ScottishBook155.scheduledSuccessor (S : ProtectedStage (1 / 2)) (y : S.target.carrier) : ProtectedTransition S 1

The canonical successor transition which ensures that y is hit.

Equations

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

theorem ScottishBook155.scheduledSuccessor_hits (S : ProtectedStage (1 / 2)) (y : S.target.carrier) : ∃ (x : (scheduledSuccessor S y).next.source.carrier), (scheduledSuccessor S y).next.map x = (scheduledSuccessor S y).targetEmbedding y

theorem ScottishBook155.scheduledSuccessor_source_mk_le (S : ProtectedStage (1 / 2)) (y : S.target.carrier) (hM : Cardinal.mk S.source.carrier ≤ stageCardinal) : Cardinal.mk (scheduledSuccessor S y).next.source.carrier ≤ stageCardinal

theorem ScottishBook155.scheduledSuccessor_target_mk_le (S : ProtectedStage (1 / 2)) (y : S.target.carrier) (hM : Cardinal.mk S.source.carrier ≤ stageCardinal) (hN : Cardinal.mk S.target.carrier ≤ stageCardinal) : Cardinal.mk (scheduledSuccessor S y).next.target.carrier ≤ stageCardinal

theorem ScottishBook155.bentSeedStage_source_mk_le : Cardinal.mk bentSeedStage.source.carrier ≤ stageCardinal

theorem ScottishBook155.bentSeedStage_target_mk_le : Cardinal.mk bentSeedStage.target.carrier ≤ stageCardinal