frespects_eq — Mathlib

English

If f2 a2 = f2 b2, then FRespects f2 tr a2 b1 is equivalent to FRespects f2 tr b2 b1 for all b1.

Русский

Если f2 a2 = f2 b2, то FRespects f2 tr a2 b1 эквивалентно FRespects f2 tr b2 b1 для всех b1.

LaTeX

$$$\\forall {\\sigma_1 \\sigma_2} {f_2 : \\sigma_2 \\to \\mathrm{Option}\\,\\sigma_2} {tr : \\sigma_1 \\to \\sigma_2} {a_2 b_2}, f_2\\ a_2 = f_2\\ b_2 \\Rightarrow \\forall {b_1},\\ FRespects f_2 tr a_2 b_1 \\Leftrightarrow FRespects f_2 tr b_2 b_1$$$

Lean4

theorem frespects_eq {σ₁ σ₂} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} {a₂ b₂} (h : f₂ a₂ = f₂ b₂) :
    ∀ {b₁}, FRespects f₂ tr a₂ b₁ ↔ FRespects f₂ tr b₂ b₁
  | some _ => reaches₁_eq h
  | none => by unfold FRespects; rw [h]

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