congr_arg — Mathlib

English

If x = x', then applying a linear isometry equivalence to both sides preserves equality.

Русский

Если x = x', то применение линейной изометрической эквивалентности к обеим сторонам сохраняет равенство.

LaTeX

$$$\\text{congr_arg}_{f}(x,x') : x=x' \\Rightarrow f x = f x'$$$

Lean4

protected theorem congr_arg {f : E ≃ₛₗᵢ[σ₁₂] E₂} : ∀ {x x' : E}, x = x' → f x = f x'
  | _, _, rfl => rfl

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