congrOrderIso — Mathlib

English

For an order isomorphism e, certain equivalences of finite congruence hold, preserving order-related relations.

Русский

Для изоморфизма порядка e сохраняются эквивалентности для конечных классов, сохраняющие порядок.

LaTeX

$$$\forall e, \text{ congrOrderIso } e : \ldots$$$

Lean4

/-- An `OrderIso` on `MulArchimedeanClass` induces an `OrderIso` on `FiniteMulArchimedeanClass`. -/
@[to_additive /-- An `OrderIso` on `ArchimedeanClass` induces an `OrderIso` on `FiniteArchimedeanClass`. -/
    ]
noncomputable def congrOrderIso (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) :
    FiniteMulArchimedeanClass M ≃o FiniteMulArchimedeanClass N
    where
  __ := Equiv.subtypeEquiv e (by simp)
  map_rel_iff' := by simp

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