English
An equivalence between a Respects predicate on f1,f2 and a family of FRespects conditions parameterized by a function tr.
Русский
Эквивалентность между отношением Respects на f1,f2 и семейством условий FRespects, параметризованных функцией tr.
LaTeX
$$$\\forall {\\sigma_1 \\sigma_2 f_1 f_2} {tr : \\sigma_1 \\to \\sigma_2},\\\\n (\\mathrm{Respects} f_1 f_2 (\\lambda a b => tr\\ a = b)) \\\\n \\leftrightarrow \\forall {a_1}, \\mathrm{FRespects} f_2 tr (tr\\ a_1) (f_1\\ a_1)$$$
Lean4
theorem fun_respects {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂} :
(Respects f₁ f₂ fun a b ↦ tr a = b) ↔ ∀ ⦃a₁⦄, FRespects f₂ tr (tr a₁) (f₁ a₁) :=
forall_congr' fun a₁ ↦ by cases f₁ a₁ <;> simp only [FRespects, exists_eq_left', forall_eq']
