Icc_map_sectL

Mathlib.Order.Interval.Finset.Basic

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

English

For any a,b and c, mapping Icc by the left-section with c yields the product-interval Icc(a,c) to Icc(b,c).

Русский

Для любых a,b и c отображение Icc по секции слева даёт интервал Icc(a,c) до Icc(b,c).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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