covBy_iff_wcovBy_and_not_le

Mathlib.Order.Cover

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

English

A is covered by B if and only if A is weakly covered by B and not B ≤ A.

Русский

A⋖B эквивалентно A ⩿ B и ¬(B ≤ A).

LaTeX

$$$ a \\,⋖\\, b \\iff (a ⩿ b) \\land \\neg (b \\le a) $$$

Lean4

theorem covBy_iff_wcovBy_and_not_le : a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a :=
  ⟨fun h => ⟨h.wcovBy, h.lt.not_ge⟩, fun h => h.1.covBy_of_not_le h.2⟩

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

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

Разделы

Аффилиация

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