equiv — Mathlib

English

For any α and Encodable α, there is an equivalence α ≃ ULower α given by Encodable.equivRangeEncode α.

Русский

Для любого типа α с кодируемостью существует эквиваленция α ≃ ULower α, задаваемая Encodable.equivRangeEncode α.

LaTeX

$$$ \alpha \simeq ULower(\alpha) $$$

Lean4

/-- The equivalence between the encodable type `α` and `ULower α : Type`. -/
def equiv : α ≃ ULower α :=
  Encodable.equivRangeEncode α

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