instLawfulSingleton — Mathlib

English

There is a canonical LawfulSingleton structure on Set α, arising from the singleton operation on subsets of α.

Русский

Существует каноническая структура LawfulSingleton над множеством Set α, возникающая из операции единичного множества над подмножествами α.

LaTeX

$$$\text{LawfulSingleton} \ (\,\text{Set }\alpha\,)$$$

Lean4

instance : LawfulSingleton α (Set α) :=
  ⟨fun x =>
    Set.ext fun a => by
      simp only [mem_empty_iff_false, mem_insert_iff, or_false]
      exact Iff.rfl⟩

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