liouvilleWith — Mathlib

English

A Liouville number x with exponent p is LiouvilleWith p x for every real p.

Русский

Число Лиувилля x с показателем p является LiouvilleWith p x для любого действительного p.

LaTeX

$$$$ \forall x \in \mathbb{R},\; Liouville(x) \Rightarrow \forall p \in \mathbb{R},\; LiouvilleWith(p,x). $$$$

Lean4

/-- A Liouville number is a Liouville number with any real exponent. -/
protected theorem liouvilleWith (hx : Liouville x) (p : ℝ) : LiouvilleWith p x :=
  by
  suffices LiouvilleWith ⌈p⌉₊ x from this.mono (Nat.le_ceil p)
  refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
  rintro b ⟨_hb, a, hne, hlt⟩
  refine ⟨a, hne, ?_⟩
  rwa [rpow_natCast]

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