neg_strictAnti — Mathlib

English

The negation map a ↦ -a is strictly decreasing on EReal.

Русский

Отображение отрицания a ↦ -a строго убывающее на EReal.

LaTeX

$$$$ \\text{StrictAnti}(-\\cdot : \\mathrm{EReal} \\to \\mathrm{EReal}) $$$$

Lean4

theorem neg_strictAnti : StrictAnti (-· : EReal → EReal) :=
  WithBot.strictAnti_iff.2
    ⟨WithTop.strictAnti_iff.2 ⟨coe_strictMono.comp_strictAnti fun _ _ => neg_lt_neg, fun _ => bot_lt_coe _⟩,
      WithTop.forall.2 ⟨bot_lt_top, fun _ => coe_lt_top _⟩⟩

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