mabs_dite — Mathlib

English

Absolute value commutes with a dependent if-then-else: |if h : p then a h else b h|_m = if h : p then |a h|_m else |b h|_m.

Русский

Модуль сохраняется сквозь зависимое ветвление: |if h : p then a h else b h|_м = если h : p то |a h|_м иначе |b h|_м.

LaTeX

$$|if h : p then a h else b h|_m = if h : p then |a h|_m else |b h|_m$$

Lean4

@[to_additive]
theorem mabs_dite (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) :
    |if h : p then a h else b h|ₘ = if h : p then |a h|ₘ else |b h|ₘ :=
  apply_dite _ _ _ _

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