Ico_coe_coe

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#WithTop.Ico_coe_coe

English

The Ico interval in WithTop between a and b is the image of Ico(a,b) under the some embedding.

Русский

Ico интервал между a и b в WithTop является образом Ico(a,b) через some.

LaTeX

$$$ Ico\,(a : WithTop\,\alpha)\,b = (Ico\,a\,b) \mapsto_{\text{some}} $$$

Lean4

theorem Ico_coe_coe : Ico (a : WithTop α) b = (Ico a b).map Embedding.some :=
  rfl

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

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

Разделы

Аффилиация

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