reaches₁_eq — Mathlib

English

If f a = f b, then Reaches₁ f a c ↔ Reaches₁ f b c for any a,b,c.

Русский

Если f a = f b, тогда Reaches₁ f a c эквивалентно Reaches₁ f b c для любых a,b,c.

LaTeX

$$$\\forall a\\,b\\,c,\\ (f\\ a = f\\ b) \\Rightarrow (Reaches_1\\ f\\ a\\ c \\iff Reaches_1\\ f\\ b\\ c)$$$

Lean4

theorem reaches₁_eq {σ} {f : σ → Option σ} {a b c} (h : f a = f b) : Reaches₁ f a c ↔ Reaches₁ f b c :=
  TransGen.head'_iff.trans (TransGen.head'_iff.trans <| by rw [h]).symm

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