swap — Mathlib

English

If h is a derivation from b to a in r, then there is a derivation from a to b in the swapped relation.

Русский

Если есть цепочка от b к a по r, то существует цепочка от a к b по swapped r.

LaTeX

$$$$\\forall {α} {r : α \\to α \\to \\mathrm{Prop}} {a b} (h : \\operatorname{TransGen} r b a), \\operatorname{TransGen} (swap r) a b$$$$

Lean4

theorem swap (h : TransGen r b a) : TransGen (swap r) a b := by
  induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc

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