instSubsingleton — Mathlib

English

The data expressing that (a,b) is a kernel pair is subsingleton; i.e., any two witnesses are equal.

Русский

Данные, устанавливающие, что (a,b) образуют KernelPair, образуют подподмножество; то есть любые два доказательства совпадают.

LaTeX

$$Subsingleton (IsKernelPair f a b)$$

Lean4

/-- The data expressing that `(a, b)` is a kernel pair is subsingleton. -/
instance : Subsingleton (IsKernelPair f a b) :=
  ⟨fun P Q => by constructor⟩

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