instMeasurableSingletonClass — Mathlib

English

If α has a MeasurableSingletonClass, then the Subtype p also has it.

Русский

Если у пространства α есть свойство измеримойsingleton, то и подтип p обладает им.

LaTeX

$$$\\text{MeasurableSingletonClass}(\\mathrm{Subtype}(p))$$$

Lean4

instance instMeasurableSingletonClass {p : α → Prop} [MeasurableSingletonClass α] : MeasurableSingletonClass (Subtype p)
    where
  measurableSet_singleton
    x :=
    ⟨{(x : α)}, measurableSet_singleton (x : α), by rw [← image_singleton, preimage_image_eq _ Subtype.val_injective]⟩

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