lt_mul_exp_iff_le — Mathlib

English

Let x,y be elements of the multiplicative integers with zero, with y ≠ 0. Then x < y·exp(1) if and only if x ≤ y.

Русский

Пусть x,y принадлежат к почти целочисленной группе с нулём в мультипликативной форме; если y ≠ 0, то x < y·exp(1) тогда и только тогда, когда x ≤ y.

LaTeX

$$$\forall x,y \in \mathbb{Z}^{\times}_{0},\ y\neq 0:\ x < y\cdot \exp(1) \iff x \le y.$$$

Lean4

theorem lt_mul_exp_iff_le {x y : ℤᵐ⁰} (hy : y ≠ 0) : x < y * exp 1 ↔ x ≤ y :=
  by
  lift y to Multiplicative ℤ using hy
  obtain rfl | hx := eq_or_ne x 0
  · simp
  lift x to Multiplicative ℤ using hx
  rw [← log_le_log, ← log_lt_log] <;> simp [log_mul, Int.lt_add_one_iff]

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