measurableAtom_eq_of_mem — Mathlib

English

If x lies in the atom of y, then the atoms are equal.

Русский

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

LaTeX

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

Lean4

theorem measurableAtom_eq_of_mem {x y : β} (hx : x ∈ measurableAtom y) : measurableAtom x = measurableAtom y :=
  by
  refine subset_antisymm (measurableAtom_subset_of_mem hx) ?_
  by_cases hy : y ∈ measurableAtom x
  · exact measurableAtom_subset_of_mem hy
  exfalso
  simp only [measurableAtom, mem_iInter, not_forall] at hx hy ⊢
  obtain ⟨s, hxs, hs, hys⟩ := hy
  specialize hx sᶜ hys hs.compl
  exact hx hxs

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