toLower_le_toLower

Mathlib.Topology.Order.LowerUpperTopology

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

English

For x,y in WithLower α, ofLower x ≤ ofLower y iff x ≤ y in the induced order.

Русский

Для x,y в WithLower α, ≤ в α эквивалентно ≤ в WithLower α через toLower и instPreorder.

LaTeX

$$$\\Forall {x,y: WithLower α},\\; ofLower x ≤ ofLower y \\iff x ≤ y$$$

Lean4

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

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

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

Разделы

Аффилиация

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