English
A product over products is a product indexed by a product; a two-level product is again a product.
Русский
Произведение над произведениями является произведением, индексируемым произведением; двухуровневое произведение снова является произведением.
LaTeX
$$$\text{prod}:\;\text{IsLimit } c' \to \text{IsLimit } c$$$
Lean4
/-- A product over products is a product indexed by a product. -/
def prod (c : ∀ i : ι, Fan (fun j : ι' ↦ X i j)) (hc : ∀ i : ι, IsLimit (c i)) (c' : Fan (fun i : ι ↦ (c i).pt))
(hc' : IsLimit c') : (IsLimit <| Fan.mk c'.pt fun p : ι × ι' ↦ c'.proj _ ≫ (c p.1).proj p.2) :=
by
refine mkFanLimit _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
· exact Fan.IsLimit.desc hc' fun i ↦ Fan.IsLimit.desc (hc i) fun j ↦ t.proj (i, j)
· simp
· refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
exact Fan.IsLimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))
