toLower_lt_toLower

Mathlib.Topology.Order.LowerUpperTopology

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

English

Similarly, toLower preserves strict order: toLower x < toLower y iff x < y.

Русский

Аналогично: toLower сохраняет строгий порядок: toLower x < toLower y эквивалентно x < y.

LaTeX

$$$\\forall {x,y: α},\\; toLower x < toLower y \\iff x < y$$$

Lean4

@[simp]
theorem toLower_lt_toLower {x y : α} : toLower x < toLower y ↔ x < y :=
  .rfl

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

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

Разделы

Аффилиация

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