notMem_range_embeddingUpIntGE_iff

English

Similarly, the image of UpIntGE misses a value exactly when that value is strictly greater than p.

Русский

Аналогично, образ UpIntGE пропускает значение точно тогда, когда оно строго больше p.

LaTeX

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

Lean4

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

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