toUpper_symm

Mathlib.Topology.Order.LowerUpperTopology

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

English

The inverse of toUpper is exactly the map ofUpper; i.e., toUpper is invertible with inverse ofUpper.

Русский

Обратная к toUpper равна toUpper обратное — фактически это отображение ofUpper.

LaTeX

$$$\\operatorname{toUpper} \\text{.symm} = \\operatorname{ofUpper}$$$

Lean4

@[simp]
theorem toUpper_symm {α} : (@toUpper α).symm = ofUpper :=
  rfl

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

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

Разделы

Аффилиация

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