English
The entire construction ensures a nonempty Φ.Iteration j for every j, via the recursive decomposition provided by mkOfBot, mkOfSucc, and mkOfLimit.
Русский
Вся конструкция гарантирует не пустой Φ.Iteration j для каждого j по рекурсивному разбору mkOfBot, mkOfSucc, mkOfLimit.
LaTeX
$$$\\forall j, \\; \\exists x: Φ.Iteration j$$$
Lean4
/-- When `j` is a limit element, this is the element in `Φ.Iteration j`
that is constructed from elements in `Φ.Iteration i` for all `i < j`. -/
noncomputable def mkOfLimit {j : J} (hj : Order.IsSuccLimit j) (iter : ∀ (i : J), i < j → Φ.Iteration i) : Φ.Iteration j
where
F := functor hj iter
obj_bot := functor_obj hj iter ⊥ (Order.IsSuccLimit.bot_lt hj) (mkOfBot Φ J) (by rfl)
arrowSucc_eq i
hi := by
rw [arrowSucc_def, arrowMap_functor _ _ _ _ (Order.le_succ i) ((Order.IsSuccLimit.succ_lt_iff hj).2 hi),
arrow_mk_mapObj, ← arrowSucc_def _ _ ((Order.lt_succ_of_le_of_not_isMax (by rfl) (not_isMax_of_lt hi))),
arrowSucc_eq, functor_obj _ _ _ hi]
arrowMap_limit i hi hij k
hk := by
obtain hij | rfl := hij.lt_or_eq
· rw [arrowMap_functor _ _ _ _ _ hij, arrow_mk_mapObj, arrowMap_limit _ _ hi _ _ hk]
congr 1
apply Arrow.functor_ext
rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
dsimp
generalize_proofs
rw [← arrowMap, ← arrowMap, arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij), arrow_mk_mapObj]
apply congr_arrowMap
· rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi]
congr 1
apply Arrow.functor_ext
rintro ⟨l₁, hl₁⟩ ⟨l₂, hl₂⟩ f
dsimp
generalize_proofs
rw [← arrowMap, arrow_mk_mapObj, arrowMap_functor _ _ _ _ _ hl₂, arrow_mk_mapObj]
