instHomClassOfOrderHomClass — Mathlib

English

Every map f of type F between ordered structures that preserves relations is monotone, i.e. x ≤ y implies f(x) ≤ f(y).

Русский

Любая функция f между упорядоченными структурами, сохраняющая отношение порядка, монотонна: если x ≤ y, то f(x) ≤ f(y).

LaTeX

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

Lean4

instance [FunLike F M N] [OrderHomClass F M N] : Language.order.HomClass F M N :=
  ⟨fun _ => isEmptyElim,
    by
    simp only [forall_relations, relation_eq_leSymb, relMap_leSymb, Fin.isValue, Function.comp_apply]
    exact fun φ x => map_rel φ⟩
    -- If `OrderEmbeddingClass` or `RelEmbeddingClass` is defined, this should be generalized.

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