coe_star

Mathlib.Topology.ContinuousMap.Star

URI: https://scilib.ai/kg/mathlib#ContinuousMap.coe_star

English

The coe of star f equals the star of the coe of f: coe(star f) = star (coe f).

Русский

Проекция (coe) звездf равна звезде проекции f: coe(star f) = star (coe f).

LaTeX

$$$\\mathrm{coe}\\,(\\mathrm{star}\\; f) = \\mathrm{star}\\, (\\mathrm{coe}\\; f)$$$

Lean4

@[simp]
theorem coe_star (f : C(α, β)) : ⇑(star f) = star (⇑f) :=
  rfl

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

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

Разделы

Аффилиация

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