disjoint_residual_ae — Mathlib

English

The residual filter on R and the almost-everywhere volume measure are disjoint.

Русский

Резидентный фильтр наℝ и мера объема, определяемая почти повсюду, не пересекаются.

LaTeX

$$$$ \text{Disjoint}(\text{residual } \mathbb{R}, \text{ae } \text{volume}). $$$$

Lean4

/-- The filters `residual ℝ` and `ae volume` are disjoint. This means that there exists a residual
set of Lebesgue measure zero (e.g., the set of Liouville numbers). -/
theorem disjoint_residual_ae : Disjoint (residual ℝ) (ae volume) :=
  disjoint_of_disjoint_of_mem disjoint_compl_right eventually_residual_liouville ae_not_liouville

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