isSeparable_ae_range — Mathlib

English

A.e. range of an AEStronglyMeasurable function is contained in a separable set.

Русский

Предел по а.е. диапазона AEStronglyMeasurable функции лежит в сепарабельном множестве.

LaTeX

$$$\exists t:\\ Set β, IsSeparable t \\land ∀ᵐ x ∂\mu, f x ∈ t$$$

Lean4

theorem isSeparable_ae_range (hf : AEStronglyMeasurable f μ) : ∃ t : Set β, IsSeparable t ∧ ∀ᵐ x ∂μ, f x ∈ t :=
  by
  refine ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩
  filter_upwards [hf.ae_eq_mk] with x hx
  simp [hx]

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