mk_monotoneOn — Mathlib

English

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

Русский

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

LaTeX

$$MonotoneOn mk (Set.Iic (1))$$

Lean4

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

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