cast_strictMono — Mathlib

English

The map x ↦ x viewed as an element of K is strictly increasing on ℚ≥0; i.e., if p < q in ℚ≥0 then (p : K) < (q : K).

Русский

Отображение x ↦ x (как элемент K) строго возрастает на ℚ≥0: если p < q, то (p : K) < (q : K).

LaTeX

$$$\text{StrictMono}(\uparrow): \mathbb{Q}_{\ge 0} \to K$$$

Lean4

theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun p q h =>
  by
  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul, Nat.cast_lt (α := K), ←
    NNRat.lt_def]
  · simp
  · simp

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