English
If a relation tr is respected and a1 is related to a2, and b1 ∈ eval f1 a1, then there exists b2 with tr b1 b2 and b2 ∈ eval f2 a2.
Русский
Если tr сохраняет переходы и a1 связан с a2 через tr, и b1 принадлежит eval f1 a1, то существует b2 с tr b1 b2 и b2 ∈ eval f2 a2.
LaTeX
$$$\\forall {f_1 f_2 tr} (H : Respects f_1 f_2 tr) \\forall {a_1 a_2} (aa : tr a_1 a_2) (ab : b_1 \\in eval f_1 a_1),\\ exists b_2, tr b_1 b_2 \\wedge b_2 \\in eval f_2 a_2$$$
Lean4
theorem tr_eval {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂ → Prop} (H : Respects f₁ f₂ tr) {a₁ b₁ a₂} (aa : tr a₁ a₂)
(ab : b₁ ∈ eval f₁ a₁) : ∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂ :=
by
obtain ⟨ab, b0⟩ := mem_eval.1 ab
rcases tr_reaches H aa ab with ⟨b₂, bb, ab⟩
refine ⟨_, bb, mem_eval.2 ⟨ab, ?_⟩⟩
have := H bb; rwa [b0] at this
