instSubsingletonOfIsEmpty — Mathlib

English

If β is empty, Kernel α β is a subsingleton; all kernels are equal.

Русский

Если β пусто, ядро α → β образует единое множество (субоднозначное); все ядра равны.

LaTeX

$$$[IsEmpty \\\\beta] \\\\Rightarrow \\\\forall \\\\kappa_1, \\\\kappa_2: Kernel(\\\\alpha, \\\\beta), \\\\kappa_1 = \\\\kappa_2$$$

Lean4

instance [IsEmpty β] : Subsingleton (Kernel α β) where allEq κ η := by ext a s; simp [Set.eq_empty_of_isEmpty s]

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