English
There is a canonical equivalence between the product piLT X i × X i and the Pi over the lower cone {j ≤ i}.
Русский
Существует каноническое эквивалентное соответствие между произведением piLT X i × X i и произведением по всей нижней окрестности {j ≤ i}.
LaTeX
$$$\\mathrm{piSplitLE}\\; f : \\mathrm{piLT}X i \\times X i \\simeq (j: (Set.Iic i).Elem) \\to X j$$$
Lean4
/-- Splitting off the `X i` factor from the Pi type over `{j | j ≤ i}`. -/
def piSplitLE : piLT X i × X i ≃ ∀ j : Iic i, X j
where
toFun f j := if h : j = i then h.symm ▸ f.2 else f.1 ⟨j, j.2.lt_of_ne h⟩
invFun f := (fun j ↦ f ⟨j, j.2.le⟩, f ⟨i, le_rfl⟩)
left_inv f := by ext j; exacts [dif_neg j.2.ne, dif_pos rfl]
right_inv f := by grind
