finLiftOn_empty — Mathlib

English

The empty-index case reduces to a trivial evaluation principle for Trunc.

Русский

Пустой индекс сводит к тривиальному принципу оценки для Trunc.

LaTeX

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

Lean4

@[simp]
theorem finLiftOn_empty [e : IsEmpty ι] (q : ∀ i, Trunc (α i)) : finLiftOn (β := β) q = fun f _ ↦ f e.elim :=
  funext₂ fun _ _ ↦ congrFun₂ (Quotient.finLiftOn_empty q) _ _

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