range_eq_univ — Mathlib

English

The range of a bijection e: α ≃ β is the whole codomain β; equivalently, the associated function is surjective.

Русский

Область значений биекции e: α ≃ β равна всей области β; эквивалентно соответствующая функция сюръективна.

LaTeX

$$$\operatorname{range}(e) = \mathrm{univ}.$$$

Lean4

@[simp]
theorem range_eq_univ {α : Type*} {β : Type*} {E : Type*} [EquivLike E α β] (e : E) : range e = univ :=
  eq_univ_of_forall (EquivLike.toEquiv e).surjective

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