instStrongHomClassOfOrderIsoClass

English

An equivalence-like structure between ordered sets yields an order-isomorphism class, i.e. maps that preserve order form an OrderIsoClass.

Русский

Гомоморфизмы, сохраняя порядок, формируют класс OrderIso между упорядоченными множествами.

LaTeX

$$$ \text{OrderIsoClass } F M N $$$

Lean4

instance [EquivLike F M N] [OrderIsoClass F M N] : Language.order.StrongHomClass F M N :=
  ⟨fun _ => isEmptyElim, by
    simp only [order.forall_relations, order.relation_eq_leSymb, relMap_leSymb, Fin.isValue, Function.comp_apply,
      map_le_map_iff, implies_true]⟩

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