equivRange_symm_apply_mk — Mathlib

English

The symmetric of equivRange evaluated at f(x) equals x, i.e., the inverse mapping recovers the original value.

Русский

Симметрика equivRange в точке f(x) возвращает x, то есть обратное отображение восстанавливает исходное значение.

LaTeX

$$$\\mathrm{hf.equivRange}^{-1}(\\langle f(x), \\text{mem\\_range}(x)\\rangle) = x$$$

Lean4

@[simp]
theorem equivRange_symm_apply_mk (hf : MeasurableEmbedding f) (x : α) :
    hf.equivRange.symm ⟨f x, mem_range_self x⟩ = x :=
  by
  nth_rw 3 [← hf.equivRange.symm_apply_apply x]
  rw [hf.equivRange_apply]

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