isGE_iff — Mathlib

English

IsGE and IsLE are equivalent to the corresponding exactness statements across all degrees.

Русский

IsGE и IsLE эквивалентны соответствующим условиям точности во всех степенях.

LaTeX

$$$K.IsGE(n) \iff \forall in, K.ExactAt(i)$$$

Lean4

theorem isGE_iff (n : ℤ) : K.IsGE n ↔ ∀ (i : ℤ) (_ : i < n), K.ExactAt i :=
  by
  constructor
  · intro _ i hi
    exact K.exactAt_of_isGE n i hi
  · intro h
    refine IsSupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

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