notMem_range_embeddingUpIntLE_iff

English

The image of the embedding UpIntLE misses a particular integer precisely when that integer lies below the shift bound p.

Русский

Образ вложения UpIntLE пропускает конкретное целое число точно тогда, когда оно лежит ниже порога сдвига p.

LaTeX

$$$(\\forall i:\\mathbb{N}, f(i)\\neq n) \\iff p

Lean4

theorem notMem_range_embeddingUpIntLE_iff (n : ℤ) : (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n :=
  by
  constructor
  · intro h
    by_contra!
    exact h (p - n).natAbs (by simp; cutsat)
  · intros
    dsimp
    cutsat

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