English
If a relation tr is respected by f1,f2, and a1 is related to a2 via tr, and a1 reaches b1 via f1, then there exists b2 related to b1 by tr such that a2 reaches b2 via f2.
Русский
Если отображение сохраняет переходы, и a1 связан с a2 через tr, и a1 достигает b1 через f1, тогда существует b2, связанное с b1 через tr, такое что a2 достигает b2 через f2.
LaTeX
$$$\\forall {f_1 f_2 tr} (H : Respects f_1 f_2 tr) \\forall {a_1 a_2}, tr\\ a_1 a_2 \\to \\forall {b_1}, Reaches_1 f_1 a_1 b_1 \\to \\exists b_2, tr b_1 b_2 \\wedge Reaches_1 f_2 a_2 b_2$$$
Lean4
theorem tr_reaches {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ a₂} (aa : tr a₁ a₂) {b₁}
(ab : Reaches f₁ a₁ b₁) : ∃ b₂, tr b₁ b₂ ∧ Reaches f₂ a₂ b₂ :=
by
rcases reflTransGen_iff_eq_or_transGen.1 ab with (rfl | ab)
· exact ⟨_, aa, ReflTransGen.refl⟩
· have ⟨b₂, bb, h⟩ := tr_reaches₁ H aa ab
exact ⟨b₂, bb, h.to_reflTransGen⟩
