sign_neg — Mathlib

English

Let α be an additive group with a preorder, decidable LT, and AddRightStrictMono. Then for every a in α, sign(-a) = -sign(a).

Русский

Пусть α — упорядоченная абелева группа с правой строгой монотонностью. Тогда для любого a ∈ α выполняется sign(-a) = -sign(a).

LaTeX

$$$ \forall a \in \alpha,\ \operatorname{sign}(-a) = -\operatorname{sign}(a). $$$

Lean4

theorem sign_neg [AddRightStrictMono α] (a : α) : sign (-a) = -sign a :=
  by
  simp_rw [sign_apply, Right.neg_pos_iff, Right.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

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