to_nil — Mathlib

English

If a tree t is bounded between o1 and o2, then the empty tree nil is bounded between the same bounds.

Русский

Если дерево t ограничено между o1 и o2, то пустое дерево nil ограничено теми же границами.

LaTeX

$$$\forall t\ o_1\ o_2: Bounded\ t\ o_1\ o_2 \Rightarrow Bounded\ nil\ o_1\ o_2$$$

Lean4

theorem to_nil {t : Ordnode α} : ∀ {o₁ o₂}, Bounded t o₁ o₂ → Bounded nil o₁ o₂
  | none, _, _ => ⟨⟩
  | some _, none, _ => ⟨⟩
  | some _, some _, h => h.to_lt

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