ofLawson

Mathlib.Topology.Order.LawsonTopology

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

English

ofLawson is the identity equivalence between WithLawson α and α.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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