sign_comp — Mathlib

English

If f is strictly monotone and preserves zero, then sign(f(a)) = sign(a) for all a.

Русский

Если f строго монотонна и сохраняет ноль, то sign(f(a)) = sign(a) для всякого a.

LaTeX

$$$\\forall a,\\ sign(f(a)) = sign(a)$, \\text{whenever } f \\text{ is strictly monotone and zero-preserving.$$

Lean4

/-- `SignType.sign` respects strictly monotone zero-preserving maps. -/
theorem sign_comp {β F : Type*} [Zero β] [Preorder β] [DecidableLT β] [FunLike F α β] [ZeroHomClass F α β] {f : F}
    (hf : StrictMono f) (a : α) : sign (f a) = sign a := by simp only [sign_apply, ← map_zero f, hf.lt_iff_lt]

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