mk — Mathlib · SciLib

English

There is a witness set S such that μ(S) = 0 and ν(S^c) = 0 in the mutually singular framework.

Русский

Существуют множества S такие, что μ(S) = 0 и ν(S^c) = 0 в рамках взаимной ортогональности.

LaTeX

$$$\exists S\ (\mu S = 0 \wedge \nu S^c = 0)$$$

Lean4

theorem mk {s t : Set α} (hs : μ s = 0) (ht : ν t = 0) (hst : univ ⊆ s ∪ t) : MutuallySingular μ ν :=
  by
  use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs
  refine measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx ?_) ht
  exact subset_toMeasurable _ _ hxs

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