alternatizeUncurryFin_constOfIsEmptyLIE_comp

English

Zero-dimensional special case reduces to a subsingleton construction.

Русский

Особый нулевомерный случай сводится к конструированию subsingleton.

LaTeX

$$$\\text{alternatizeUncurryFin} (\\text{constOfIsEmptyLIE } 𝕜 E F (\\text{Fin }0) \\circ_L f) = \\text{ofSubsingleton } 𝕜 E F 0\, f$$$

Lean4

theorem alternatizeUncurryFin_constOfIsEmptyLIE_comp (f : E →L[𝕜] F) :
    alternatizeUncurryFin (constOfIsEmptyLIE 𝕜 E F (Fin 0) ∘L f) = ofSubsingleton _ _ _ (0 : Fin 1) f :=
  by
  ext
  simp [alternatizeUncurryFin_apply]

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