reverse_surjective

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.reverse_surjective

English

The reverse map is surjective on the set of compositions.

Русский

Обратное отображение сюръективно на множестве композиций.

LaTeX

$$$\\mathrm{reverse}$ is surjective: \\forall c, \\exists d, \\mathrm{reverse}(d) = c.$$$

Lean4

theorem reverse_surjective : Function.Surjective (@reverse n) :=
  reverse_involutive.surjective

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

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

Разделы

Аффилиация

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