isLE_iff — Mathlib

English

K.IsLE n holds iff K is supported up to level n, i.e., K.ExactAt i holds for all i > n.

Русский

K.IsLE n эквивалентно тому, что K поддержан до уровня n, т.е. K.ExactAt i для всех i > n.

LaTeX

$$$K.IsLE(n) \iff \forall i>n, K.ExactAt(i)$$$

Lean4

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

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