oneLePart_eq_ite — Mathlib

English

For all α in a linear-ordered group, the positive part equals the value of an if-then-else on the comparison to 1: a⁺ᵐ = ite(1 ≤ a, a, 1).

Русский

Для элементов в линейно упорядоченной группе положительная часть равна ite(1 ≤ a, a, 1).

LaTeX

$$a^{+m} = \operatorname{ite}(1 \le a, a, 1)$$

Lean4

@[to_additive]
theorem oneLePart_eq_ite : a⁺ᵐ = if 1 ≤ a then a else 1 := by rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault];
  simp_rw [sup_comm]

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