ofBijective_apply — Mathlib

English

For any a in A1, applying the promoted isomorphism yields the same as applying f: (ofBijective f hf) a = f a.

Русский

Для любого элемента a ∈ A1 применение продвинутого изоморфизма совпадает с применением f: (ofBijective f hf) a = f a.

LaTeX

$$$ (\\mathrm{ofBijective}(f, hf))\\, a = f\\, a \\quad (a \\in A_1)$$$

Lean4

theorem ofBijective_apply (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) (a : A₁) : (ofBijective f hf) a = f a :=
  rfl

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