withTopOrderIso_apply_coe — Mathlib

English

Applying withTopOrderIso to a finite class returns the underlying finite class value.

Русский

Применение withTopOrderIso к конечному классу возвращает его неизменное значение.

LaTeX

$$$withTopOrderIso M (A : WithTop (FiniteMulArchimedeanClass M)) = A.val$$$

Lean4

@[to_additive (attr := simp)]
theorem withTopOrderIso_apply_coe (A : FiniteMulArchimedeanClass M) :
    withTopOrderIso M (A : WithTop (FiniteMulArchimedeanClass M)) = A.val :=
  WithTop.subtypeOrderIso_apply_coe A

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