sInf_add — Mathlib

English

Let p: N → Prop be a predicate. If n is at most the infimum of {m ∈ N : p(m)}, then shifting the predicate by n preserves the infimum up to a subtraction of n, i.e. sInf{m ∈ N : p(m+n)} + n = sInf{m ∈ N : p(m)}.

Русский

Пусть p: ℕ → ℙ – предикат. Если n ≤ infimum множества {m ∈ ℕ : p(m)}, то сдвиг предиката на n сохраняет инфимум: sInf{m ∈ ℕ : p(m+n)} + n = sInf{m ∈ ℕ : p(m)}.

LaTeX

$$$\\inf\\{m \\in \\mathbb{N} : p(m+n)\\} + n = \\inf\\{m \\in \\mathbb{N} : p(m)\\}$, \\quad \\text{при } n \\le \\inf\\{m \\in \\mathbb{N} : p(m)\\}.$$

Lean4

theorem sInf_add {n : ℕ} {p : ℕ → Prop} (hn : n ≤ sInf {m | p m}) : sInf {m | p (m + n)} + n = sInf {m | p m} := by
  classical
  obtain h | ⟨m, hm⟩ := {m | p (m + n)}.eq_empty_or_nonempty
  · rw [h, Nat.sInf_empty, zero_add]
    obtain hnp | hnp := hn.eq_or_lt
    · exact hnp
    suffices hp : p (sInf {m | p m} - n + n) from (h.subset hp).elim
    rw [Nat.sub_add_cancel hn]
    exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
  · have hp : ∃ n, n ∈ {m | p m} := ⟨_, hm⟩
    rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
    rw [Nat.sInf_def hp] at hn
    exact find_add hn

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