ofUpper_toUpper

Mathlib.Topology.Order.LowerUpperTopology

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

English

The inverse direction: ofUpper (toUpper a) = a for all a ∈ α.

Русский

Обратное направление: ofUpper (toUpper a) = a для всех a ∈ α.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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