projIcc_of_le_left

Mathlib.Order.Interval.Set.ProjIcc

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

English

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

Русский

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

LaTeX

$$projIcc_of_le_left(h, x) = ⟨a, left_mem_Icc.2 h⟩$$

Lean4

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

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

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

Разделы

Аффилиация

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