withTopOrderIso — Mathlib

English

An order isomorphism between MulArchimedeanClass M and MulArchimedeanClass N induces an order isomorphism between FiniteMulArchimedeanClass M and FiniteMulArchimedeanClass N.

Русский

Изоморфизм порядка между MulArchimedeanClass M и MulArchimedeanClass N индуцирует изоморфизм порядка между FiniteMulArchimedeanClass M и FiniteMulArchimedeanClass N.

LaTeX

$$$\text{congrOrderIso } e : FiniteMulArchimedeanClass M \congo FiniteMulArchimedeanClass N$$$

Lean4

/-- Adding top to the type of finite classes yields the type of all classes. -/
@[to_additive /-- Adding top to the type of finite classes yields the type of all classes. -/
    ]
noncomputable def withTopOrderIso : WithTop (FiniteMulArchimedeanClass M) ≃o MulArchimedeanClass M :=
  WithTop.subtypeOrderIso

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