exists_not_and_succ_of_not_zero_of_exists

English

If p is not satisfied somewhere near zero, then there exists an n with ¬p n and p(n+1).

Русский

Если не выполняется p около нуля, то существует n, для которого ¬p n и p(n+1).

LaTeX

$$$$ \forall {p:\mathbb{N}\to \mathsf{Prop}}, \neg p(0) \rightarrow (\exists n, \neg p(n) \land p(n+1)). $$$$

Lean4

theorem exists_not_and_succ_of_not_zero_of_exists {p : ℕ → Prop} (H' : ¬p 0) (H : ∃ n, p n) : ∃ n, ¬p n ∧ p (n + 1) :=
  by
  classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)

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