English
If c1 and c2 are limit fans and bc is a limit binary fan on their cone points, then the fan built from combPairHoms is a limit cone.
Русский
Если c1 и c2 — пределы-фаны, а bc — ограниченный двузвенный фан на их конусных точках, то фан, построенный из combPairHoms, является пределом.
LaTeX
$$$ \\text{combPairIsLimit} : IsLimit (Fan.mk bc.pt (combPairHoms c1 c2 bc))$$$
Lean4
/-- If `c₁` and `c₂` are limit fans and `bc` is a limit binary fan on their cone
points, then the fan constructed from `combPairHoms` is a limit cone. -/
def combPairIsLimit : IsLimit (Fan.mk bc.pt (combPairHoms c₁ c₂ bc)) :=
mkFanLimit _
(fun s ↦
Fan.IsLimit.desc h <| fun i ↦ by
cases i
· exact Fan.IsLimit.desc h₁ (fun a ↦ s.proj (.inl a))
· exact Fan.IsLimit.desc h₂ (fun a ↦ s.proj (.inr a)))
(fun s w ↦ by
cases w <;>
· simp only [fan_mk_proj, combPairHoms]
erw [← Category.assoc, h.fac]
simp only [pair_obj_left, mk_pt, mk_π_app, IsLimit.fac])
(fun s m hm ↦
Fan.IsLimit.hom_ext h _ _ <| fun w ↦ by
cases w
· refine Fan.IsLimit.hom_ext h₁ _ _ (fun a ↦ by aesop)
· refine Fan.IsLimit.hom_ext h₂ _ _ (fun a ↦ by aesop))
