ae_eval_ne — Mathlib

English

For any i with NoAtoms(μ_i), and any x ∈ α_i, almost surely y_i ≠ x under the product measure.

Русский

Для любого i с NoAtoms(μ_i) и любого x ∈ α_i, почти наверняка y_i ≠ x по произведённой мере.

LaTeX

$$$\forall i,\,[\mathrm{NoAtoms}(\mu_i)]\Rightarrow \forall x,\ \mathsf{ae}(y_i \neq x)\text{ under } (\pi\mu)$$$

Lean4

theorem ae_eval_ne (i : ι) [NoAtoms (μ i)] (x : α i) : ∀ᵐ y : ∀ i, α i ∂Measure.pi μ, y i ≠ x :=
  compl_mem_ae_iff.2 (pi_hyperplane μ i x)

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