mem_measurableSet_iff — Mathlib

English

Let x,y ∈ γ be inseparable. If s is a Borel measurable subset of γ, then x ∈ s iff y ∈ s.

Русский

Пусть x,y ∈ γ — inseparable точки. Тогда для любого измеримого множества s ⊆ γ выполняется x ∈ s ⇔ y ∈ s.

LaTeX

$$$\\\\forall x,y\\\\in\\\\gamma\\\\,\\\\ Inseparable(x,y)\\\\Rightarrow\\\\forall s\\\\subseteq\\\\gamma\\\\,\\\\MeasurableSet(s)\\\\Rightarrow (x\\\\in s\\\\iff y\\\\in s).$$$

Lean4

/-- If two points are topologically inseparable,
then they can't be separated by a Borel measurable set. -/
theorem mem_measurableSet_iff {x y : γ} (h : Inseparable x y) {s : Set γ} (hs : MeasurableSet s) : x ∈ s ↔ y ∈ s :=
  MeasurableSet.induction_on_open (fun _ ↦ h.mem_open_iff) (fun _ _ ↦ Iff.not) (fun _ _ _ h ↦ by simp [h]) s hs

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