ite_apply — Mathlib

English

The value of a piecewise function at a point equals the corresponding branch evaluated at that point.

Русский

Значение кусочно-заданной функции в точке равно соответствующему ветвлению, рассчитанному в этой точке.

LaTeX

$$$\text{The value of } \mathrm{ite}(P,f,g) \text{ at } x \text{ equals } \begin{cases} f, & P \text{ true} \\ g, & P \text{ false} \end{cases} (x).$$$

Lean4

theorem ite_apply {P : Prop} [Decidable P] (f g : F) (x : α) : (if P then f else g) x = if P then f x else g x :=
  dite_apply _ _ _

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