exists_measurableSet_of_ne — Mathlib

English

Let α be a type equipped with a measurable structure that separates points. For any distinct x and y in α, there exists a measurable set s with x ∈ s and y ∉ s.

Русский

Пусть α — множество с измеримым пространством, которое разделяет точки. Для любых различных x и y в α существует измеримое множество s, такое что x ∈ s и y ∉ s.

LaTeX

$$$ \\forall {\\alpha} [MeasurableSpace \\alpha] [SeparatesPoints \\alpha] (x,y : \\alpha) (h : x \\neq y), \\exists s, MeasurableSet s \\land x \\in s \\land y \\notin s $$$

Lean4

theorem exists_measurableSet_of_ne [MeasurableSpace α] [SeparatesPoints α] {x y : α} (h : x ≠ y) :
    ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s := by
  contrapose! h
  exact separatesPoints_def h

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