range_val — Mathlib

English

The range of the projection from a subtype to α is the set s itself.

Русский

Образ проекции из подтипа в α равен s.

LaTeX

$$$ \operatorname{range}(\operatorname{Subtype.val}) = s $$$

Lean4

/-- A variant of `range_coe`. Try to use `range_coe` if possible.
  This version is useful when defining a new type that is defined as the subtype of something.
  In that case, the coercion doesn't fire anymore. -/
theorem range_val {s : Set α} : range (Subtype.val : s → α) = s :=
  range_coe

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