covariant_le_iff_contravariant_lt

English

In LinearOrder N, Covariant with ≤ is equivalent to Contravariant with <.

Русский

В линейном порядке L Covariant по ≤ эквивалентно Contravariant по <.

LaTeX

$$$[LinearOrder\ N]\; Covariant(M,N,μ,\le) \iff Contravariant(M,N,μ,<)$$$

Lean4

theorem covariant_le_iff_contravariant_lt [LinearOrder N] : Covariant M N μ (· ≤ ·) ↔ Contravariant M N μ (· < ·) :=
  ⟨fun h _ _ _ bc ↦ not_le.mp fun k ↦ bc.not_ge (h _ k), fun h _ _ _ bc ↦ not_lt.mp fun k ↦ bc.not_gt (h _ k)⟩

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