cast_ite — Mathlib

English

For any Prop P with a decidable instance, the cast of the if-then-else expression equals the if-then-else of the casts: (ite P m n) cast = ite P (m cast) (n cast).

Русский

Для любого утверждения P с определением Decidable, приведение к R сохраняет ветвление: (ite P m n) cast = ite P (m cast) (n cast).

LaTeX

$$$ (\mathrm{ite}\ P\ m\ n : \mathbb{N}) \uparrow = \mathrm{ite}\ P\ (m \uparrow)\ (n \uparrow). $$$

Lean4

@[simp, norm_cast]
theorem cast_ite (P : Prop) [Decidable P] (m n : ℕ) : ((ite P m n : ℕ) : R) = ite P (m : R) (n : R) := by
  split_ifs <;> rfl

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