ofInjective'_apply — Mathlib

English

For a StarAlgEquiv f with an injective underlying function, the action of its injective-application form on x equals f x.

Русский

Для звездоэквивалента f с инъективной функцией отображения примененная форма действует как f на x.

LaTeX

$$$\operatorname{ofInjective'}\ f\ hf\ x = f\ x$$$

Lean4

@[simp]
theorem ofInjective'_apply (f : F) (hf : Function.Injective f) (x : A) : ofInjective' f hf x = f x :=
  rfl

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