separating_of_generateFrom — Mathlib

English

Let S be a family of subsets of α. If the σ-algebra generated by S separates points, then for any x,y, whenever x and y have the same membership pattern across all s ∈ S, we must have x = y.

Русский

Пусть S — семейство подмножеств α. Если σ-алгебра, порожденная S, разделяет точки, то для любых x,y, если для всех s ∈ S выполняется x ∈ s ↔ y ∈ s, то x = y.

LaTeX

$$$ (\\forall x,y: \\alpha, (\\forall s \\in S, x \\in s \\leftrightarrow y \\in s)) \\rightarrow x = y $$$

Lean4

/-- If the measurable space generated by `S` separates points,
then this is witnessed by sets in `S`. -/
theorem separating_of_generateFrom (S : Set (Set α)) [h : @SeparatesPoints α (generateFrom S)] :
    ∀ x y : α, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y :=
  by
  letI := generateFrom S
  intro x y hxy
  rw [← forall_generateFrom_mem_iff_mem_iff] at hxy
  exact separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

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