toFun — Mathlib

English

For a monoid M acting on α, the map y ↦ (x ↦ x • y) embeds α into the function space M → α.

Русский

При действии моноида M на α отображение y ↦ (x ↦ x • y) внедряет α в множество функций M → α.

LaTeX

$$$ (\forall y_1,y_2 \in \alpha)\Big( (\forall x \in M, x \cdot y_1 = x \cdot y_2) \Rightarrow y_1 = y_2 \Big). $$$

Lean4

/-- Embedding of `α` into functions `M → α` induced by a multiplicative action of `M` on `α`. -/
@[to_additive /-- Embedding of `α` into functions `M → α` induced by an additive action of `M` on `α`. -/
    ]
def toFun : α ↪ M → α :=
  ⟨fun y x ↦ x • y, fun y₁ y₂ H ↦ one_smul M y₁ ▸ one_smul M y₂ ▸ by convert congr_fun H 1⟩

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