English
If γ has a division operation, then extending f with g1/g2 and e1/e2 preserves division: extend f (g1 / g2) (e1 / e2) = extend f g1 e1 / extend f g2 e2.
Русский
Пусть γ имеет операцию деления. Расширение f на g1/g2 и e1/e2 сохраняет деление: extend f (g1 / g2) (e1 / e2) = extend f g1 e1 / extend f g2 e2.
LaTeX
$$$ \mathrm{extend} f (g_1 / g_2) (e_1 / e_2) = \mathrm{extend} f g_1 e_1 / \mathrm{extend} f g_2 e_2 $$$
Lean4
@[to_additive]
theorem extend_div [Div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂ := by
classical
funext x
simp [Function.extend_def, apply_dite₂]
