wcovBy_iff_covBy_or_le_and_le — Mathlib

English

A weak cover relation holds between a and b if and only if either a covers b or a = b.

Русский

A ⩿ B эквивалентно либо A ⋖ B, либо A = B.

LaTeX

$$$ a ⩿ b \\iff (a \\,⋖\\, b) \\lor (a = b) $$$

Lean4

theorem wcovBy_iff_covBy_or_le_and_le : a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a :=
  ⟨fun h => or_iff_not_imp_right.mpr fun h' => h.covBy_of_not_le fun hba => h' ⟨h.le, hba⟩, fun h' =>
    h'.elim (fun h => h.wcovBy) fun h => h.1.wcovBy_of_le h.2⟩

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