English
Let f be a function of two variables, and P decidable. The application of f to two dites is itself a dite of the two-argument function applied to each branch: f(dite P a b, dite P c d) = dite P (λ h. f (a h) (c h)) (λ h. f (b h) (d h)).
Русский
Пусть f: α → β → γ; применяя его к двум ветвям dite, мы получаем dite, в котором каждая ветвь применяет f к соответствующим веткам, т.е. ...
LaTeX
$$$f(\dite P a b)(\dite P c d) = \dite P(\lambda h. f(a h)(c h))(\lambda h. f(b h)(d h))$$$
Lean4
/-- A two-argument function applied to two `dite`s is a `dite` of that two-argument function
applied to each of the branches. -/
theorem apply_dite₂ {α β γ : Sort*} (f : α → β → γ) (P : Prop) [Decidable P] (a : P → α) (b : ¬P → α) (c : P → β)
(d : ¬P → β) : f (dite P a b) (dite P c d) = dite P (fun h ↦ f (a h) (c h)) fun h ↦ f (b h) (d h) := by
by_cases h : P <;> simp [h]
