isStrictlyLE_of_le

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

← MathLib Explorer

English

If p ≤ q and K.IsStrictlyLE p holds, then K.IsStrictlyLE q holds as well.

Русский

Если p ≤ q и K.IsStrictlyLE p выполняется, то K.IsStrictlyLE q тоже выполняется.

LaTeX

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

Lean4

theorem isStrictlyLE_of_le (p q : ℤ) (hpq : p ≤ q) [K.IsStrictlyLE p] : K.IsStrictlyLE q :=
  by
  rw [isStrictlyLE_iff]
  intro i hi
  apply K.isZero_of_isStrictlyLE p
  cutsat

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

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

Разделы

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

Аффилиация

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