isStrictlyGE_of_ge

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.isStrictlyGE_of_ge

← MathLib Explorer

English

If p ≤ q and K.IsStrictlyGE q, then K.IsStrictlyGE p.

Русский

Если p ≤ q и K.IsStrictlyGE q, то K.IsStrictlyGE p.

LaTeX

$$If p ≤ q, then K.IsStrictlyGE q ⇒ K.IsStrictlyGE p$$

Lean4

theorem isStrictlyGE_of_ge (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyGE q] : K.IsStrictlyGE p :=
  by
  rw [isStrictlyGE_iff]
  intro i hi
  apply K.isZero_of_isStrictlyGE q
  cutsat

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru