up — Mathlib · SciLib

English

The identity function provides a natural equivalence between Set α and SetSemiring α.

Русский

Естественная эквивалентность между Set α и SetSemiring α задаётся тождественным отображением.

LaTeX

$$$\operatorname{up}: \{\text{Set }\alpha\} \to \{\text{SetSemiring }\alpha\}$ is the identity-based equivalence.$$

Lean4

/-- The identity function `Set α → SetSemiring α`. -/
protected def up : Set α ≃ SetSemiring α :=
  Equiv.refl _

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