boundaryLE_embeddingUpIntLE_iff — Mathlib

English

Similarly, the boundary-left condition for embeddingUpIntLE is equivalent to n=0, reflecting the LE counterpart of the boundary condition.

Русский

Аналогично, условие BoundaryLE для embeddingUpIntLE эквивалентно n=0, отражая LE-подобное условие границы.

LaTeX

$$$(\\text{embeddingUpIntLE }p).BoundaryLE n \\leftrightarrow n=0$$$

Lean4

theorem boundaryLE_embeddingUpIntLE_iff (p : ℤ) (n : ℕ) : (embeddingUpIntLE p).BoundaryLE 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

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