mem_gt — Mathlib

English

If t is bounded between x and o, then every element of t is greater than x.

Русский

Если дерево t ограничено между x и o, то каждый элемент t больше x.

LaTeX

$$$\forall t\ x\ o: Bounded\ t\ x\ o \Rightarrow All(> x)\ t$$$

Lean4

theorem mem_gt : ∀ {t o} {x : α}, Bounded t x o → All (· > x) t
  | nil, _, _, _ => ⟨⟩
  | node _ _ _ _, _, _, ⟨h₁, h₂⟩ => ⟨h₁.mem_gt, h₁.to_lt, h₂.mem_gt.imp fun _ => lt_trans h₁.to_lt⟩

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