covBy_iff_wcovBy_and_lt

Mathlib.Order.Cover

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

English

A is covered by B if and only if A is weakly covered by B and A < B.

Русский

A⋖B эквивалентно A ⩿ B и A < B.

LaTeX

$$$ a \\,⋖\\, b \\iff (a ⩿ b) \\land (a < b) $$$

Lean4

theorem covBy_iff_wcovBy_and_lt : a ⋖ b ↔ a ⩿ b ∧ a < b :=
  ⟨fun h => ⟨h.wcovBy, h.lt⟩, fun h => h.1.covBy_of_lt h.2⟩

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

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

Разделы

Аффилиация

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