English
Let p: ℕ → Prop be a predicate with sInf{m : ℕ | p m} > 0. Then sInf{m | p m} + n = sInf{m | p(m − n)} for all n, provided this is well-defined in ℕ.
Русский
Пусть p: ℕ → ℙ и sInf{m:ℕ | p m} > 0. Тогда для любого n выполняется sInf{m | p m} + n = sInf{m | p(m − n)} (при условии корректности в ℕ).
LaTeX
$$$\\text{If } 0 < \\inf\\{m \\in \\mathbb{N} : p(m)\\} ,\\text{ then } \\inf\\{m \\in \\mathbb{N} : p(m)\\} + n = \\inf\\{m \\in \\mathbb{N} : p(m-n)\\}.$$$
Lean4
theorem sInf_add' {n : ℕ} {p : ℕ → Prop} (h : 0 < sInf {m | p m}) : sInf {m | p m} + n = sInf {m | p (m - n)} :=
by
suffices h₁ : n ≤ sInf {m | p (m - n)} by
convert sInf_add h₁
simp_rw [Nat.add_sub_cancel_right]
obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
refine
le_csInf ⟨m + n, ?_⟩ fun b hb ↦
le_of_not_gt fun hbn ↦ ne_of_mem_of_not_mem ?_ (notMem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)
· dsimp
rwa [Nat.add_sub_cancel_right]
· exact hb
