monotone — Mathlib

English

As above, any map with a monotone structure is monotone.

Русский

Как и ранее, любая монотонная структура сохраняется в виде монотонной функции.

LaTeX

$$$ \text{Monotone } f $$$

Lean4

theorem monotone [Preorder M] [L.OrderedStructure M] [Preorder N] [L.OrderedStructure N] (f : F) : Monotone f :=
  fun a b => by
  have h := HomClass.map_rel f leSymb ![a, b]
  simp only [relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Function.comp_apply] at h
  exact h

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