to_lt

Mathlib.Data.Ordmap.Invariants

URI: https://scilib.ai/kg/mathlib#Ordnode.Bounded.to_lt

← MathLib Explorer

English

If t is bounded between x and y, then x < y.

Русский

Если дерево ограничено между x и y, то x < y.

LaTeX

$$$\forall t\ x\ y: Bounded\ t\ x\ y \Rightarrow x < y$$$

Lean4

theorem to_lt : ∀ {t : Ordnode α} {x y : α}, Bounded t x y → x < y
  | nil, _, _, h => h
  | node _ _ _ _, _, _, ⟨h₁, h₂⟩ => lt_trans h₁.to_lt h₂.to_lt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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