mk_le_mk_iff_lt — Mathlib

English

If a ≠ 1, then mk a ≤ mk b is equivalent to there exists n such that |b|_m < |a|_m^n.

Русский

Пусть a ≠ 1. Тогда mk a ≤ mk b эквивалентно существованию натурального числа n такого, что |b|_м < |a|_м^n.

LaTeX

$$$(a \neq 1) \Rightarrow (mk\ a \le mk\ b \iff \exists n \in \mathbb{N},\ |b|_m < |a|_m^n)$$$

Lean4

@[to_additive]
theorem mk_le_mk_iff_lt (ha : a ≠ 1) : mk a ≤ mk b ↔ ∃ n, |b|ₘ < |a|ₘ ^ n :=
  by
  refine ⟨fun ⟨n, hn⟩ ↦ ⟨n + 1, hn.trans_lt ?_⟩, fun ⟨n, hn⟩ ↦ ?_⟩
  · rw [pow_succ]
    exact lt_mul_of_one_lt_right' _ (one_lt_mabs.mpr ha)
  · exact ⟨n, hn.le⟩

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