projIcc_right

Mathlib.Order.Interval.Set.ProjIcc

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

English

projIcc_right: projection at x=b yields the right endpoint.

Русский

projIcc_right: проекция в x=b даёт правую границу.

LaTeX

$$projIcc_right(h) = ⟨b, right_mem_Icc.2 h⟩$$

Lean4

@[simp]
theorem projIcc_right : projIcc a b h b = ⟨b, right_mem_Icc.2 h⟩ :=
  projIcc_of_right_le h le_rfl

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

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

Разделы

Аффилиация

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