step_invRev_iff — Mathlib

English

Red.Step (invRev L1) (invRev L2) holds if and only if Red.Step L1 L2 holds.

Русский

Red.Step (invRev L1) (invRev L2) выполняется тогда и только тогда, когда Red.Step L1 L2 выполняется.

LaTeX

$$$Red.Step (invRev\\ L_1) (invRev\\ L_2) \\iff Red.Step\\ L_1\\ L_2$$$

Lean4

@[to_additive (attr := simp)]
theorem step_invRev_iff : Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) ↔ Red.Step L₁ L₂ :=
  ⟨fun h => by simpa only [invRev_invRev] using h.invRev, fun h => h.invRev⟩

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