map'_mono — Mathlib

English

If α has an AddZeroClass structure and left-monotone addition, then WithZero α also inherits a left-monotone addition.

Русский

Если у α есть структура AddZeroClass и левая монотонность сложения, то WithZero α наследует левую монотонность сложения.

LaTeX

$$$ \text{AddLeftMono}(\mathrm{WithZero} \alpha) $$$

Lean4

theorem map'_mono [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : Monotone f) : Monotone (map' f) := by
  simpa [Monotone, WithZero.forall]

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