projIci_of_le

Mathlib.Order.Interval.Set.ProjIcc

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

English

If x ≤ a, then projIci(a, x) = ⟨a, le_rfl⟩.

Русский

Если x ≤ a, то projIci(a, x) = ⟨a, le_rfl⟩.

LaTeX

$$projIci(a,x) = ⟨a, le_rfl⟩, when x ≤ a.$$

Lean4

theorem projIci_of_le (hx : x ≤ a) : projIci a x = ⟨a, le_rfl⟩ :=
  Subtype.ext <| max_eq_left hx

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

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

Разделы

Аффилиация

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