ofBijective_apply — Mathlib

English

For x in range f, the inverse of the bijective equivalence sends x back to its preimage, i.e., f((ofBijective f h).symm x) = x.

Русский

Для x в образе f обратная карта биективной эквивалентности возвращает x в исходное: f((ofBijective f h).symm x)=x.

LaTeX

$$$f((\\mathrm{ofBijective}\\,f\\,h).\\mathrm{symm}(x))=x \\quad (x \\in \\mathrm{range}(f)).$$$

Lean4

@[simp]
theorem ofBijective_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf} (x : M) : ofBijective f hf x = f x :=
  rfl

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