covBy_of_ne

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.covBy_of_ne

English

In a preorder, if a ⩿ b and a ≠ b, then a ⋖ b.

Русский

В предпорядке, если a ⩿ b и a ≠ b, тогда a ⋖ b.

LaTeX

$$$ (a ⩿ b) \\land (a \\ne b) \\Rightarrow a \\,⋖\\, b $$$

Lean4

theorem covBy_of_ne (h : a ⩿ b) (h2 : a ≠ b) : a ⋖ b :=
  ⟨h.le.lt_of_ne h2, h.2⟩

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

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

Разделы

Аффилиация

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