map'_strictMono — Mathlib

English

If f is monotone (respecting order), then the induced map on WithZero α to WithZero β is monotone.

Русский

Если f монотонна, то индуцированная карта на WithZero α → WithZero β монотонна.

LaTeX

$$$ \text{map' } f \text{ is monotone given } f \text{ is monotone}$$$

Lean4

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

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