English
A dite producing a Pi-type, when applied to a value a, equals a dite that applies the branch to a: (dite P f g) a = dite P (λ h. f h a) (λ h. g h a).
Русский
Dite, порождающее Π-тип, при применении к значению a равно dite, применяющее ветку к a: (dite P f g) a = dite P (λ h. f h a) (λ h. g h a).
LaTeX
$$$\,(dite P f g)\ a = dite P (\lambda h. f h a) (\lambda h. g h a)$$$
Lean4
/-- A 'dite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `dite` that applies
either branch to `a`. -/
theorem dite_apply (f : P → ∀ a, σ a) (g : ¬P → ∀ a, σ a) (a : α) :
(dite P f g) a = dite P (fun h ↦ f h a) fun h ↦ g h a := by by_cases h : P <;> simp [h]
