ofLower_toLower

Mathlib.Topology.Order.LowerUpperTopology

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

English

Applying toLower to an element of α gives the same element under the equivalence.

Русский

Применение toLower к элементу α даёт тот же элемент в эквивалентности.

LaTeX

$$$toLower(a) = a$ under equivalence$$

Lean4

@[simp]
theorem ofLower_toLower (a : α) : ofLower (toLower a) = a :=
  rfl

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

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

Разделы

Аффилиация

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