projIcc_eq_left

Mathlib.Order.Interval.Set.ProjIcc

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

English

projIcc(a,b,h,x) equals the left endpoint iff x ≤ a when a < b.

Русский

projIcc(a,b,h,x) равно левой границе эквивалентно x ≤ a при a < b.

LaTeX

$$projIcc_eq_left(h,x) : projIcc(a,b,h,x) = ⟨a, left_mem_Icc.2 h⟩ ↔ x ≤ a$$

Lean4

theorem projIcc_eq_left (h : a < b) : projIcc a b h.le x = ⟨a, left_mem_Icc.mpr h.le⟩ ↔ x ≤ a := by
  simp [projIcc, Subtype.ext_iff, h.not_ge]

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

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

Разделы

Аффилиация

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