ite_apply — Mathlib

English

An ite producing a Pi-type, when applied to a value a, equals an ite that applies the corresponding function to a: (ite P f g) a = ite P (f a) (g a).

Русский

Ite создаёт Pi-тип; применяя к значению a, получаем: (ite P f g) a = ite P (f a) (g a).

LaTeX

$$$ (\ite P f g)\ a = \ite P (f a) (g a) $$$

Lean4

/-- A 'ite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `ite` that applies
either branch to `a`. -/
theorem ite_apply (f g : ∀ a, σ a) (a : α) : (ite P f g) a = ite P (f a) (g a) :=
  dite_apply P (fun _ ↦ f) (fun _ ↦ g) a

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