apply_eq_zero_of_not_le

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

URI: https://scilib.ai/kg/mathlib#IncidenceAlgebra.apply_eq_zero_of_not_le

English

If a is not less or equal to b, then f a b = 0 for any f in the incidence algebra.

Русский

Если a не менее или равно b, тогда для любого f из инцидентной алгебры f a b = 0.

LaTeX

$$$ (\forall a,b, \neg a \le b) \Rightarrow f a b = 0 $$$

Lean4

theorem apply_eq_zero_of_not_le (h : ¬a ≤ b) (f : IncidenceAlgebra 𝕜 α) : f a b = 0 :=
  eq_zero_of_not_le' _ h

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

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

Разделы

Аффилиация

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