range_coe — Mathlib

English

The range of the canonical embedding equals the elements strictly below top.

Русский

Область значений канонического вложения равна элементам строго меньшим верхнего.

LaTeX

$$$ \operatorname{range}({\text{some}}) = \{ y \mid y < \top \} $$$

Lean4

theorem range_coe : range (some : α → WithTop α) = Iio ⊤ :=
  by
  ext x
  rw [mem_Iio, WithTop.lt_top_iff_ne_top, mem_range, ne_top_iff_exists]

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