instIsNonstrictStrictOrderWCovByCovBy

English

The pair of relations (weak cover, cover) forms a nonstrict-strict order on the set.

Русский

Пара отношений (⊩ слабое покрытие, ⋖ покрытие) образует ненасыщенный строгий порядок на множестве.

LaTeX

$$$ IsNonstrictStrictOrder\\, \\alpha\\, (\\,⩿\\,): (⋖) $$$

Lean4

instance : IsNonstrictStrictOrder α (· ⩿ ·) (· ⋖ ·) :=
  ⟨fun _ _ => covBy_iff_wcovBy_and_not_le.trans <| and_congr_right fun h => h.wcovBy_iff_le.not.symm⟩

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