equiv — Mathlib

English

The equivalence LevyProkhorov.equiv provides an equivalence between LevyProkhorov α and α.

Русский

Эквивалентность LevyProkhorov.equiv задаёт эквивалентность между LevyProkhorov α и α.

LaTeX

$$$$ \mathrm{equiv}(\alpha) : LevyProkhorov(\alpha) \cong \alpha. $$$$

Lean4

/-- The "identity" equivalence between the type synonym `LevyProkhorov α` and `α`. -/
def equiv (α : Type*) : LevyProkhorov α ≃ α :=
  Equiv.refl _

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