id_comp — Mathlib

English

Let f be a cocompact map. Composing f on the left with the identity cocompact map on the domain yields f unchanged; i.e., the left identity for composition holds.

Русский

Пусть f — коккомпактное отображение. При композиции слева с тождественным коккомпактным отображением на области получаем то же отображение f.

LaTeX

$$$ \mathrm{id}_{\alpha} \circ f = f $$$

Lean4

@[simp]
theorem id_comp (f : CocompactMap α β) : (CocompactMap.id _).comp f = f :=
  ext fun _ => rfl

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