orderAddMonoidHom_apply — Mathlib

English

The evaluation of the order-embedded map equals the evaluation of the standard addMonoidHom map: for all x ∈ G, (orderAddMonoidHom G)(x) = (addMonoidHom G)(x).

Русский

Значение отображения, введённого с сохранением порядка, равно значению стандартного addMonoidHom: для всех x ∈ G выполняется (orderAddMonoidHom G)(x) = (addMonoidHom G)(x).

LaTeX

$$$$ \forall x \in G,\; (orderAddMonoidHom\ G)(x) = (addMonoidHom\ G)(x). $$$$

Lean4

@[simp]
theorem orderAddMonoidHom_apply (x : G) : orderAddMonoidHom G x = addMonoidHom G x :=
  rfl

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