toLawson

Mathlib.Topology.Order.LawsonTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLawson.toLawson

English

toLawson is the identity equivalence between α and WithLawson α.

Русский

toLawson — тождественная эквивергенция между α и WithLawson α.

LaTeX

$$$\text{toLawson} : \alpha \simeq \mathrm{WithLawson}\alpha.$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru