lift_apply_of — Mathlib

English

The lift map sends the generator image to its label: lift f (of x) = f x.

Русский

Каркасный отображение подводит генератор к его значению: lift f (of x) = f x.

LaTeX

$$$\\forall x,\\ lift f (of\\ x) = f(x)$$$

Lean4

@[simp]
theorem lift_apply_of (x : α) : lift f (of x) = f x :=
  by
  convert Abelianization.lift_apply_of (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x)
  exact (FreeGroup.lift_apply_of (β := Multiplicative β)).symm

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