instFunLike

Mathlib.Topology.Homotopy.HomotopyGroup

URI: https://scilib.ai/kg/mathlib#GenLoop.instFunLike

English

A structural lemma ensuring the compatibility of the FunLike instance with equality of underlying functions.

Русский

Лемма совместимости инстанса FunLike с равенством базовых функций.

LaTeX

$$GenLoop.instFunLike.match_1 : …$$

Lean4

instance instFunLike : FunLike (Ω^ N X x) (I^N) X where
  coe f := f.1
  coe_injective' := fun ⟨⟨f, _⟩, _⟩ ⟨⟨g, _⟩, _⟩ _ => by congr

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

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

Разделы

Аффилиация

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