pos_size_of_mem — Mathlib

English

If t is Sized and x belongs to t, then the size of t is strictly positive.

Русский

Если t удовлетворяет Sized и x принадлежит t, то размер t положителен.

LaTeX

$$$t\text{ Sized} \land x \in t \implies 0 < \operatorname{size}(t)$$$

Lean4

theorem pos_size_of_mem [LE α] [DecidableLE α] {x : α} {t : Ordnode α} (h : Sized t) (h_mem : x ∈ t) : 0 < size t := by
  cases t;
  · { contradiction
  };
  · { simp [h.1]
  }

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