Theorems · Theorem · number theory

setOf_liouvilleWith_subset_aux

Deprecated since 2026-07-09Use setOfPred_liouvilleWith_subset_aux instead.

{x | ∃ p > 2, LiouvilleWith p x} ⊆
  ⋃ m,
    (fun x => x + ↑m) ⁻¹'
      ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}

Alias of setOfPred_liouvilleWith_subset_aux.

Defined in

Mathlib.NumberTheory.Transcendental.Liouville.Measure

Cited by

0 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound