measurableAtom_subset_of_mem — Mathlib

English

If x lies in the atom of y, then the atom of x is contained in the atom of y.

Русский

Если x принадлежит атому y, то атом x содержится в атоме y.

LaTeX

$$$$ x \in \operatorname{measurableAtom}(y) \Rightarrow \operatorname{measurableAtom}(x) \subseteq \operatorname{measurableAtom}(y) $$$$

Lean4

/-- There is in fact equality: see `measurableAtom_eq_of_mem`. -/
theorem measurableAtom_subset_of_mem {x y : β} (hx : x ∈ measurableAtom y) : measurableAtom x ⊆ measurableAtom y :=
  by
  intro z hz
  simp only [measurableAtom, mem_iInter] at hz hx ⊢
  exact fun s hys hs ↦ hz s (hx s hys hs) hs

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