pos_size_of_mem — Mathlib

English

If an element x is in a nonempty Ordset t, then the size of t is positive: 0 < size(t).

Русский

Если элемент x принадлежит Ordset t, тогда размер t положителен: 0 < size(t).

LaTeX

$$$$ x\\in t \\Rightarrow 0<\\operatorname{size}(t). $$$$

Lean4

theorem pos_size_of_mem {x : α} {t : Ordset α} (h_mem : x ∈ t) : 0 < size t :=
  by
  simp only [Membership.mem, mem, Bool.decide_eq_true] at h_mem
  apply Ordnode.pos_size_of_mem t.property.sz h_mem

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