measurableSet_cut — Mathlib

English

For any relation r, the set of a with r(a, f(a)) is measurable when fibers are measurable.

Русский

Для любого отношения r множество {a : α | r(a, f(a))} измеримо при условии, что множества волокон измеримы.

LaTeX

$$$\\{a : α \\mid r(a, f(a))\\}$ измеримо$$

Lean4

theorem measurableSet_cut (r : α → β → Prop) (f : α →ₛ β) (h : ∀ b, MeasurableSet {a | r a b}) :
    MeasurableSet {a | r a (f a)} :=
  by
  have : {a | r a (f a)} = ⋃ b ∈ range f, {a | r a b} ∩ f ⁻¹' { b } :=
    by
    ext a
    suffices r a (f a) ↔ ∃ i, r a (f i) ∧ f a = f i by simpa
    exact ⟨fun h => ⟨a, ⟨h, rfl⟩⟩, fun ⟨a', ⟨h', e⟩⟩ => e.symm ▸ h'⟩
  rw [this]
  exact MeasurableSet.biUnion f.finite_range.countable fun b _ => MeasurableSet.inter (h b) (f.measurableSet_fiber _)

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