ae_not_liouvilleWith — Mathlib

English

Almost every real x has no LiouvilleWith p x for any exponent p (i.e., for almost every x and every p>2, LiouvilleWith p x fails).

Русский

Почти каждое действительное число x не удовлетворяет условию LiouvilleWith p x для любого показателя p>2.

LaTeX

$$$$ \forall^{\mathrm{ae}} x \in \mathbb{R}, \; \forall p>2, \; \neg LiouvilleWith(p,x). $$$$

Lean4

theorem ae_not_liouvilleWith : ∀ᵐ x, ∀ p > (2 : ℝ), ¬LiouvilleWith p x := by
  simpa only [ae_iff, not_forall, Classical.not_not, setOf_exists] using volume_iUnion_setOf_liouvilleWith

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