lift_t — Mathlib

English

In the lifting construction, the image of the stable letter t under lift is the distinguished element x.

Русский

При построении лифта изображение устойчивой буквы t — это заранее заданный элемент x.

LaTeX

$$$ \\text{lift } f\_{} x\_{} hx\_{} (t) = x $$$

Lean4

@[simp]
theorem lift_t (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : lift f x hx t = x := by
  delta HNNExtension; simp [lift, t]

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