toUpper_ofUpper

Mathlib.Topology.Order.LowerUpperTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithUpper.toUpper_ofUpper

English

The round-trip through toUpper and ofUpper is the identity on WithUpper α.

Русский

Петля через toUpper и ofUpper даёт тождественное отображение на WithUpper α.

LaTeX

$$$\\forall a : WithUpper α,\\ toUpper (ofUpper a) = a$$$

Lean4

@[simp]
theorem toUpper_ofUpper (a : WithUpper α) : toUpper (ofUpper a) = a :=
  rfl

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

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

Разделы

Аффилиация

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