wcovBy_iff_covBy_or_eq — Mathlib

English

Let a and b be elements of a partially ordered set. Then a is weakly covered by b iff either a = b or a is covered by b (CovBy a b).

Русский

Пусть 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_covBy_or_eq : a ⩿ b ↔ a ⋖ b ∨ a = b := by rw [le_antisymm_iff, wcovBy_iff_covBy_or_le_and_le]

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