measurableAtom_subset — Mathlib

English

If s is a measurable set with x ∈ s, then the atom at x is contained in s.

Русский

Если s — измеримое множество и x ∈ s, то атом x содержится в s.

LaTeX

$$$$ \operatorname{MeasurableSet}(s) \land x \in s \implies \operatorname{measurableAtom}(x) \subseteq s $$$$

Lean4

theorem measurableAtom_subset {s : Set β} {x : β} (hs : MeasurableSet s) (hx : x ∈ s) : measurableAtom x ⊆ s :=
  iInter₂_subset_of_subset s hx fun ⦃a⦄ ↦ (by simp [hs])

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