toUpperSet — Mathlib

English

There is a canonical equivalence between α and WithUpperSet α given by the identity map.

Русский

Существует канонический эквивалент между типом α и его расширением верхних множеств, заданный тем же тождественным отображением.

LaTeX

$$$\alpha \cong \mathrm{WithUpperSet}(\alpha)$$$

Lean4

/-- `toUpperSet` is the identity function to the `WithUpperSet` of a type. -/
@[match_pattern]
def toUpperSet : α ≃ WithUpperSet α :=
  Equiv.refl _

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