toEquivRange_apply — Mathlib

English

For any a in α, the image under toEquivRange is the pair (f a, mem_range_self a).

Русский

Для любого a из α образ под toEquivRange есть пара (f(a), доказательство того, что a входит в диапазон).

LaTeX

$$$f^{\text{toEquivRange}}(a) = \langle f(a), \mathrm{Set.mem\_range\_self}(a)\rangle$$$

Lean4

@[simp]
theorem toEquivRange_apply (a : α) : f.toEquivRange a = ⟨f a, Set.mem_range_self a⟩ :=
  rfl

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