Ico_map_sectL

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Ico_map_sectL

English

Mapping Ico by the left-section with c yields Ico(a,c) to Ico(b,c).

Русский

Отображение Ico по секции слева с c даёт Ico(a,c) до Ico(b,c).

LaTeX

$$$$ (Ico\ a\ b).map(\mathrm{sectL}\ c) = Ico(a,c)(b,c) $$$$

Lean4

theorem Ico_map_sectL : (Ico a b).map (.sectL _ c) = Ico (a, c) (b, c) := by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

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

Разделы

Аффилиация

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