equivRange_apply — Mathlib

English

For a measurable embedding f, the equivRange applied to x gives the pair (f(x), evidence that x is in range).

Русский

Для измеримого вложения f применение equivRange к x дает пару (f(x), доказательство, что x принадлежит диапазону).

LaTeX

$$$\\ hf.equivRange(x) = \\langle f(x), \\text{mem\\_range\_self}(x)\\rangle$$$

Lean4

@[simp]
theorem equivRange_apply (hf : MeasurableEmbedding f) (x : α) : hf.equivRange x = ⟨f x, mem_range_self x⟩ := by
  simp [MeasurableEmbedding.equivRange, MeasurableEquiv.cast, MeasurableEquiv.Set.univ, MeasurableEmbedding.equivImage]

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