Cardinal bounds at protected limit stages

theorem ScottishBook155.ProtectedChain.limitCardinalSourceDirectedSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : DirectedSystem (fun (i : ι) => (C.stage i).source.carrier) fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(C.sourceSystem.embed x1 x2 x3)

theorem ScottishBook155.ProtectedChain.limitCardinalTargetDirectedSystem {ι : Type u} [LinearOrder ι] {r L : ℝ} (C : ProtectedChain r L) : DirectedSystem (fun (i : ι) => (C.stage i).target.carrier) fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(C.targetSystem.embed x1 x2 x3)

theorem ScottishBook155.ProtectedChain.limitSource_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hι : Cardinal.mk ι ≤ stageCardinal) (hstage : ∀ (i : ι), Cardinal.mk (C.stage i).source.carrier ≤ stageCardinal) : Cardinal.mk C.LimitSource ≤ stageCardinal

theorem ScottishBook155.ProtectedChain.limitTarget_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hι : Cardinal.mk ι ≤ stageCardinal) (hstage : ∀ (i : ι), Cardinal.mk (C.stage i).target.carrier ≤ stageCardinal) : Cardinal.mk C.LimitTarget ≤ stageCardinal

theorem ScottishBook155.ProtectedChain.limitStage_source_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) (hι : Cardinal.mk ι ≤ stageCardinal) (hstage : ∀ (i : ι), Cardinal.mk (C.stage i).source.carrier ≤ stageCardinal) : Cardinal.mk (C.limitStage hr hL).source.carrier ≤ stageCardinal

theorem ScottishBook155.ProtectedChain.limitStage_target_mk_le {ι : Type u} [LinearOrder ι] [Nonempty ι] {r L : ℝ} (C : ProtectedChain r L) (hr : 0 < r) (hL : 0 < L) (hι : Cardinal.mk ι ≤ stageCardinal) (hstage : ∀ (i : ι), Cardinal.mk (C.stage i).target.carrier ≤ stageCardinal) : Cardinal.mk (C.limitStage hr hL).target.carrier ≤ stageCardinal