English
Given a fan over f with last index and a binary fan combining the last coordinate with the first, one can form a fan over all indices by stitching together the last n and the first element.
Русский
Имея фан по функции f с последним индексом и двоичный фан, соединяющий последнюю координату с первой, можно получить фан по всем индексам, объединив последние элементы с первым.
LaTeX
$$$$ \mathrm{extendFan}: \text{Fan}(f) \to \text{Fan}(f') \text{ for appropriate } f', $$$$
Lean4
/-- Given `n+1` objects of `C`, a fan for the last `n` with point `c₁.pt` and
a binary fan on `c₁.pt` and `f 0`, we can build a fan for all `n+1`.
In `extendFanIsLimit` we show that if the two given fans are limits, then this fan is also a
limit.
-/
@[simps!]
def extendFan {n : ℕ} {f : Fin (n + 1) → C} (c₁ : Fan fun i : Fin n => f i.succ) (c₂ : BinaryFan (f 0) c₁.pt) : Fan f :=
Fan.mk c₂.pt
(by
refine Fin.cases ?_ ?_
· apply c₂.fst
· intro i
apply c₂.snd ≫ c₁.π.app ⟨i⟩)
