wcovBy_iff_eq_or_covBy

Mathlib.Order.Cover

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

English

In a partially ordered set, a is weakly covered by b iff a = b or a is covered by b (CovBy a b).

Русский

В частично упорядоченном множестве a ⩿ b тогда и только тогда, когда a = b или a ⋖ b.

LaTeX

$$$a \mathrm{WCovBy} \ b \iff (a = b) \lor (a \mathrm{CovBy} \ b)$$$

Lean4

theorem wcovBy_iff_eq_or_covBy : a ⩿ b ↔ a = b ∨ a ⋖ b :=
  wcovBy_iff_covBy_or_eq.trans or_comm

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

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

Разделы

Аффилиация

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