mem_of_mem_measurableAtom — Mathlib

English

If y ∈ measurableAtom(x), then y ∈ s for every measurable set s with x ∈ s.

Русский

Если y ∈ измеримый атом x, то y ∈ s для любого измеримого множества s при условии x ∈ s.

LaTeX

$$$$ y \in \operatorname{measurableAtom}(x) \implies \forall s:\, \Set \beta, \operatorname{MeasurableSet}(s) \Rightarrow x \in s \Rightarrow y \in s $$$$

Lean4

theorem mem_of_mem_measurableAtom {x y : β} (h : y ∈ measurableAtom x) {s : Set β} (hs : MeasurableSet s)
    (hxs : x ∈ s) : y ∈ s := by
  simp only [measurableAtom, mem_iInter] at h
  exact h s hxs hs

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