separatesPoints_def — Mathlib

English

In a measurable space that separates points, if every measurable set containing x also contains y, then x = y.

Русский

В измеримом пространстве, разделяющем точки, если для каждой измеримой множества, содержащего x, содержится y, то x = y.

LaTeX

$$$ \forall x y, [MeasurableSpace \alpha], [SeparatesPoints \alpha], \left( \forall s, MeasurableSet s \rightarrow x \in s \rightarrow y \in s \right) \Rightarrow x = y $$$

Lean4

theorem separatesPoints_def [MeasurableSpace α] [hs : SeparatesPoints α] {x y : α}
    (h : ∀ s, MeasurableSet s → (x ∈ s → y ∈ s)) : x = y :=
  hs.separates _ _ h

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