exists_measurable_superset₂ — Mathlib

English

There exists a measurable superset t such that μ t = μ s and ν t = ν s.

Русский

Существет измеримое надмножество t так, что μ t = μ s и ν t = ν s.

LaTeX

$$$\exists t, s \subseteq t \wedge MeasurableSet t \wedge μ t = μ s \wedge ν t = ν s$$$

Lean4

theorem exists_measurable_superset₂ (μ ν : Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s := by
  simpa only [Bool.forall_bool.trans and_comm] using exists_measurable_superset_forall_eq (fun b => cond b μ ν) s

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