mk_antitoneOn — Mathlib

English

The map a ↦ mk(a) is antitone on the interval [1, ∞) in M; i.e., if 1 ≤ a ≤ b then mk(a) ≥ mk(b).

Русский

Отображение a ↦ mk(a) антитонично на интервале [1, ∞) в M; если 1 ≤ a ≤ b, то mk(a) ≥ mk(b).

LaTeX

$$AntitoneOn mk (Set.Ici (1))$$

Lean4

@[to_additive]
theorem mk_antitoneOn : AntitoneOn mk (Set.Ici (1 : M)) :=
  by
  intro a ha b hb hab
  contrapose! hab
  rw [mk_lt_mk] at hab
  obtain h := hab 1
  rw [mabs_eq_self.mpr ha, mabs_eq_self.mpr hb] at h
  simpa using h

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