mono — Mathlib

English

The LiouvilleWith property is invariant under multiplication by a nonzero rational, i.e., LiouvilleWith p (r · x) ↔ LiouvilleWith p x for r ≠ 0.

Русский

Свойство LiouvilleWith сохраняется при умножении на ненулевое рациональное число: LiouvilleWith p (r · x) ↔ LiouvilleWith p x, если r ≠ 0.

LaTeX

$$$ LiouvilleWith p (r \cdot x) \iff LiouvilleWith p x \quad (r \in \mathbb Q,\ r \neq 0) $$$

Lean4

/-- If a number is Liouville with exponent `p`, then it is Liouville with any smaller exponent. -/
theorem mono (h : LiouvilleWith p x) (hle : q ≤ p) : LiouvilleWith q x :=
  by
  rcases h.exists_pos with ⟨C, hC₀, hC⟩
  refine ⟨C, hC.mono ?_⟩; rintro n ⟨hn, m, hne, hlt⟩
  refine ⟨m, hne, hlt.trans_le <| ?_⟩
  gcongr
  exact_mod_cast hn

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