exists_of_count_lt_count — Mathlib

English

If count p a is strictly less than count p b, then there exists x in the interval (a,b) with p(x).

Русский

Если count p a < count p b, то существует x ∈ (a,b) с p(x).

LaTeX

$$$\operatorname{count}(p,a) < \operatorname{count}(p,b) \Rightarrow \exists x \in (a,b),\; p(x)$$$

Lean4

theorem exists_of_count_lt_count {a b : ℕ} (h : a.count p < b.count p) : ∃ x ∈ Set.Ico a b, p x :=
  by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt (lt_of_count_lt_count h)
  rw [add_assoc, count_add, Nat.lt_add_right_iff_pos] at h
  obtain ⟨t, ht, hp⟩ := count_ne_iff_exists.mp h.ne'
  simp_rw [Set.mem_Ico]
  exact ⟨a + t, by grind⟩

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