separatesPoints — Mathlib

English

If α has SeparatesPoints and s is a subset, then the subspace s inherits Separation: s SeparatesPoints.

Русский

Если у α есть разделение точек, то у подпространства s оно также имеется.

LaTeX

$$$ [MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {s : Set α} : SeparatesPoints s $$$

Lean4

instance (priority := 100) separatesPoints [MeasurableSpace α] [h : SeparatesPoints α] {s : Set α} :
    SeparatesPoints s :=
  ⟨fun _ _ hxy ↦ Subtype.val_injective <| h.1 _ _ fun _ ht ↦ hxy _ <| measurable_subtype_coe ht⟩

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