reverse_surjective — Mathlib

English

The reverse operation on walks is surjective: for every walk there exists a reverse walk that maps to it.

Русский

Операция reverse на путях сюръективна: для каждого пути существует соответствующий обратный путь.

LaTeX

$$$$\forall w:\, G.Walk,\ \exists p:\, G.Walk,\ reverse(p) = w.$$$$

Lean4

theorem reverse_surjective {u v : V} : Function.Surjective (reverse : G.Walk u v → _) :=
  RightInverse.surjective reverse_reverse

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