projIcc_of_right_le

Mathlib.Order.Interval.Set.ProjIcc

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

English

If b ≤ x, then projIcc(a,b,h,x) = ⟨b, right_mem_Icc.2 h⟩.

Русский

Если b ≤ x, то projIcc(a,b,h,x) = ⟨b, right_mem_Icc.2 h⟩.

LaTeX

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

Lean4

theorem projIcc_of_right_le (hx : b ≤ x) : projIcc a b h x = ⟨b, right_mem_Icc.2 h⟩ := by simp [projIcc, hx, h]

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

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

Разделы

Аффилиация

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