English
Given a binary function f and a decidable P, applying f to two ite expressions is equal to an ite that applies f to the corresponding branches: f(ite P a b, ite P c d) = ite P (f a c) (f b d).
Русский
Дано двусловная функция f; применение к двум выражениям if-then-else даёт снова if-then-else, но с аргументами f, т.е. ...
LaTeX
$$$f(\ite P a b)(\ite P c d) = \ite P (f a c) (f b d)$$$
Lean4
/-- A two-argument function applied to two `ite`s is a `ite` of that two-argument function
applied to each of the branches. -/
theorem apply_ite₂ {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P] (a b : α) (c d : β) :
f (ite P a b) (ite P c d) = ite P (f a c) (f b d) :=
apply_dite₂ f P (fun _ ↦ a) (fun _ ↦ b) (fun _ ↦ c) fun _ ↦ d
