projIcc_val

Mathlib.Order.Interval.Set.ProjIcc

URI: https://scilib.ai/kg/mathlib#Set.projIcc_val

English

The projection from the ray [a, ∞) onto the ambient space is surjective; its image is all elements.

Русский

Проекция из луча [a, ∞) на всю модель сюръективна; образ равен всему множеству.

LaTeX

$$$\operatorname{range}(\operatorname{projIci}(a)) = \mathrm{univ}$$$

Lean4

@[simp]
theorem projIcc_val (x : Icc a b) : projIcc a b h x = x :=
  by
  cases x
  apply projIcc_of_mem

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru