disjoint_measurableAtom_of_notMem

English

If x is not in the atom of y, then the atoms are disjoint.

Русский

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

LaTeX

$$$$ x \notin \operatorname{measurableAtom}(y) \Rightarrow \operatorname{measurableAtom}(x) \cap \operatorname{measurableAtom}(y) = \emptyset $$$$

Lean4

theorem disjoint_measurableAtom_of_notMem {x y : β} (hx : x ∉ measurableAtom y) :
    Disjoint (measurableAtom x) (measurableAtom y) :=
  by
  rw [Set.disjoint_iff_inter_eq_empty]
  ext z
  simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and]
  intro hzx hzy
  have h1 := measurableAtom_eq_of_mem hzx
  have h2 := measurableAtom_eq_of_mem hzy
  rw [← h2, h1] at hx
  exact hx (mem_measurableAtom_self x)

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