instNonemptyPush

Mathlib.Combinatorics.Quiver.Push

URI: https://scilib.ai/kg/mathlib#Quiver.instNonemptyPush

English

For any σ: V → W, if W is nonempty, then the Push σ quiver is nonempty.

Русский

Для любых σ: V → W, если W непустой, то квивер Push σ непустой.

LaTeX

$$$\\mathrm{Nonempty}(W) \\Rightarrow \\mathrm{Nonempty}(\\mathrm{Push}\\ σ)$$$

Lean4

instance [h : Nonempty W] : Nonempty (Push σ) :=
  h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru