coeFn_injective — Mathlib

English

The coercion-to-function from HomotopyWith is injective: different HomotopyWith objects determine different functions.

Русский

Сужение к функции из HomotopyWith инъективно: разные объекты HomotopyWith определяют разные функции.

LaTeX

$$$$ \text{Injective } (\text{toHomotopy}) $$$$

Lean4

theorem coeFn_injective : @Function.Injective (HomotopyWith f₀ f₁ P) (I × X → Y) (⇑) :=
  DFunLike.coe_injective'

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