coe_ofBijective — Mathlib

English

The underlying function of StarAlgEquiv.ofBijective is equal to the bijection used to create it.

Русский

Базовая функция StarAlgEquiv.ofBijective совпадает с используемым биективным отображением.

LaTeX

$$$$ \operatorname{coe\_ofBijective} : (StarAlgEquiv.ofBijective f hf : A \to B) = f. $$$$

Lean4

@[simp]
theorem coe_ofBijective {f : F} (hf : Function.Bijective f) : (StarAlgEquiv.ofBijective f hf : A → B) = f :=
  rfl

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