instSubsingletonOfForall — Mathlib

English

If the space of vertex maps V → W is a singleton, then the set of graph homomorphisms G →g H is also a singleton.

Русский

Если множество отображений вершин V→W является единичным, то множество граф-гомоморфизмов G→g H тоже единично.

LaTeX

$$$ [\\mathrm{Subsingleton}(V \\to W)] \\Rightarrow \\mathrm{Subsingleton}(G \\to_g H) $$$

Lean4

instance [Subsingleton (V → W)] : Subsingleton (G →g H) :=
  DFunLike.coe_injective.subsingleton

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