not_covBy_of_lt_of_lt

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#not_covBy_of_lt_of_lt

English

If a < b and b < c, then a is not covered by c.

Русский

Если a < b и b < c, тогда a не покрывает c.

LaTeX

$$$ (a < b) \\land (b < c) \\Rightarrow \\neg (a \\,⋖\\, c) $$$

Lean4

theorem not_covBy_of_lt_of_lt (h₁ : a < b) (h₂ : b < c) : ¬a ⋖ c :=
  (not_covBy_iff (h₁.trans h₂)).2 ⟨b, h₁, h₂⟩

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

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

Разделы

Аффилиация

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