subsingleton_of_unop — Mathlib

English

For objects A,B in Cᵒᵖ, if the hom-set from unop B to unop A is a singleton, then the hom-set from A to B in Cᵒᵖ is a subsingleton.

Русский

Для объектов A,B в Cᵒᵖ, если множество морфизмов от unop B к unop A состоит из одного элемента, то множество морфизмов от A к B в Cᵒᵖ является подсинглтонным.

LaTeX

$$$\forall A,B:\, C^{op},\; [\mathrm{Subsingleton}(\mathrm{unop} B \to \mathrm{unop} A)] \Rightarrow \mathrm{Subsingleton}(A \to B)$$$

Lean4

instance subsingleton_of_unop (A B : Cᵒᵖ) [Subsingleton (unop B ⟶ unop A)] : Subsingleton (A ⟶ B) :=
  (opEquiv A B).subsingleton

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