ofLower_symm

Mathlib.Topology.Order.LowerUpperTopology

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

English

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

Русский

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

LaTeX

$$$ofLower^{-1} = toLower$$$

Lean4

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

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

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

Разделы

Аффилиация

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