Ico_coe

Mathlib.Order.Interval.Set.WithBotTop

URI: https://scilib.ai/kg/mathlib#WithBot.Ico_coe

English

Ico at â,b̂ equals φ(Ico(a,b)).

Русский

Ico при â,b̂ равен φ(Ico(a,b)).

LaTeX

$$$ \mathrm{Ico}(\hat{a}, \hat{b}) = \phi\bigl(\mathrm{Ico}(a,b)\bigr). $$$

Lean4

theorem Ico_coe : Ico (a : WithBot α) b = (↑) '' (Ico a b) :=
  image_coe_Ico.symm

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

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

Разделы

Аффилиация

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