transGen_swap — Mathlib

English

The swapped-transGen between a and b is equivalent to the original-transGen between b and a.

Русский

Замыкание с заменой аргументов эквивалентно исходному замыканию между b и a.

LaTeX

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

Lean4

theorem transGen_swap : TransGen (swap r) a b ↔ TransGen r b a :=
  ⟨TransGen.swap, TransGen.swap⟩

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