instLawfulSingleton — Mathlib

English

If α has a MeasurableSingletonClass, then the subtype MeasurableSet has a LawfulSingleton structure: the insertion law aligns with the usual singleton construction (insert a into empty set yields {a}).

Русский

Если у α есть класс измеримых синглтонов, то подтип MeasurableSet получает структуру LawfulSingleton: закон вставки совпадает с обычной конструкцией синглтона (добавление a к пустому дает {a}).

LaTeX

$$$$\\text{LawfulSingleton } \\alpha (\\text{Subtype MeasurableSet})$$ with $$\\text{insert}(a, \\varnothing) = \\{a\\}.$$$$

Lean4

instance instLawfulSingleton [MeasurableSingletonClass α] :
    LawfulSingleton α (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨fun _ => Subtype.eq <| insert_empty_eq _⟩

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