instStrongHomClassOrderEmbedding — Mathlib

English

From an EquivLike F M N and an OrderIsoClass F M N, one obtains a StrongHomClass F M N, i.e. the maps in F act as strong order-preserving bijections.

Русский

Из эквивалентности между M и N и класса порядковых изоморфизмов следует, что F образует класс сильных гомоморфизмов между M и N.

LaTeX

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

Lean4

instance : Language.order.StrongHomClass (M ↪o N) M N :=
  ⟨fun _ => isEmptyElim, by
    simp only [order.forall_relations, order.relation_eq_leSymb, relMap_leSymb, Fin.isValue, Function.comp_apply,
      RelEmbedding.map_rel_iff, implies_true]⟩

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