boundaryGE_embeddingUpIntGE_iff — Mathlib

English

For any integer p and natural n, the embedding UpIntGE has boundaryGE exactly when n=0.

Русский

Для любого целого p и натурального n вложение UpIntGE имеет BoundaryGE тогда и только тогда, когда n=0.

LaTeX

$$$(\\text{embeddingUpIntGE }p).BoundaryGE n \\leftrightarrow n=0$$$

Lean4

theorem boundaryGE_embeddingUpIntGE_iff (p : ℤ) (n : ℕ) : (embeddingUpIntGE p).BoundaryGE n ↔ n = 0 :=
  by
  constructor
  · intro h
    obtain _ | n := n
    · rfl
    · have := h.2 n
      dsimp at this
      cutsat
  · rintro rfl
    constructor
    · simp
    · intro i hi
      dsimp at hi
      cutsat

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