nth_eq_zero_mono — Mathlib

English

If p 0 is false and a ≤ b, then nth p a = 0 implies nth p b = 0.

Русский

Если p(0) ложно и a ≤ b, тогда nth p a = 0 подразумевает nth p b = 0.

LaTeX

$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ h_0: \\\\neg p 0,\\\\ {a b}:\\\\mathbb{N},\\\\ a\\\\le b \\\\Rightarrow \\\\mathrm{nth}\\\\ p\\\\ a =0 \\\\Rightarrow \\\\mathrm{nth}\\\\ p\\\\ b =0.$$$

Lean4

theorem nth_eq_zero_mono (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) : nth p b = 0 :=
  by
  simp only [nth_eq_zero, h₀, false_and, false_or] at ha ⊢
  exact ha.imp fun hf hle => hle.trans hab

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