forall_liouvilleWith_iff — Mathlib

English

A real number x is Liouville iff it satisfies LiouvilleWith p x for every exponent p.

Русский

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

LaTeX

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

Lean4

/-- A number satisfies the Liouville condition with any exponent if and only if it is a Liouville
number. -/
theorem forall_liouvilleWith_iff {x : ℝ} : (∀ p, LiouvilleWith p x) ↔ Liouville x :=
  by
  refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
  rcases ((eventually_gt_atTop 1).and_frequently ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists with
    ⟨b, hb, a, hne, hlt⟩
  exact ⟨a, b, mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩

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