count_injective — Mathlib

English

Let p: N → Prop be a decidable predicate. If p(m) and p(n) and the counts up to m and n coincide, then m = n.

Русский

Пусть p : ℕ → ⟂ предикат с разрешимостью. Если p(m) и p(n) и число элементов x < m с p(x) равно числу элементов x < n с p(x), то m = n.

LaTeX

$$$p(m) \land p(n) \land \operatorname{count}(p,m) = \operatorname{count}(p,n) \Rightarrow m = n$$$

Lean4

theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n :=
  by
  by_contra! h : m ≠ n
  wlog hmn : m < n
  · exact this hn hm heq.symm h.symm (by grind)
  · simpa [heq] using count_strict_mono hm hmn

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