finLiftOn_empty — Mathlib

English

When the index type is empty, finLiftOn reduces to evaluation at the empty index.

Русский

Если множество индексов пустое, finLiftOn сводится к вычислению по пустому индексу.

LaTeX

$$$[e : IsEmpty ι] \\Rightarrow (\\forall q, \\ operatorname{finLiftOn} (β := β) q = \\lambda f _. f e.elim)$$$

Lean4

@[simp]
theorem finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Quotient (S i)) : finLiftOn (β := β) q = fun f _ ↦ f e.elim :=
  by
  ext f h
  dsimp [finLiftOn]
  induction finChoice q using Quotient.ind
  exact h _ _ e.elim

Похожие утверждения