toLower_symm

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLower.toLower_symm

English

The inverse of the canonical equivalence is the canonical 'ofLower' map.

Русский

Обратное отображение к канонической эквивалентности есть каноническое отображение 'ofLower'.

LaTeX

$$$(\\,toLower\\,)^{{-1}} = \\text{ofLower}$$$

Lean4

@[simp]
theorem toLower_symm : (@toLower α).symm = ofLower :=
  rfl

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

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

Разделы

Аффилиация

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