uncurry_pre — Mathlib

English

For f: B ⟶ A with B exponentiable and any X, the uncurry of ((pre f).app X) equals f ▷ (A ⟹ X) ≫ (exp.ev A).app X.

Русский

Для f: B ⟶ A с B экспоненцируемым и любого X, uncurry ((pre f).app X) = f ▷ (A ⟹ X) ≫ (exp.ev A).app X.

LaTeX

$$$\operatorname{uncurry}((\mathrm{pre} f).\mathrm{app} X) = f \triangleright (A \Rightarrow X) \;\gg\; (\exp ev\, A).\mathrm{app} X$$$

Lean4

theorem uncurry_pre (f : B ⟶ A) [Exponentiable B] (X : C) :
    CartesianClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (exp.ev A).app X := by rw [uncurry_eq, prod_map_pre_app_comp_ev]

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