lift_apply_simple — Mathlib

English

The lift sends simple generators to their images under the corresponding monoid isomorphism, i.e., cs.lift(⟨f, hf⟩)(s_i) = f(i).

Русский

Подъем отправляет простые порождающие в их образы через отображение, т.д.: cs.lift(⟨f,hf⟩)(s_i) = f(i).

LaTeX

$$cs.lift ⟨f,hf⟩ (s_i) = f(i)$$

Lean4

@[simp]
theorem lift_apply_simple {G : Type*} [Monoid G] {f : B → G} (hf : IsLiftable M f) (i : B) :
    cs.lift ⟨f, hf⟩ (s i) = f i :=
  congrFun (congrArg Subtype.val (cs.lift.left_inv ⟨f, hf⟩)) i

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