covariantClass_le_of_lt — Mathlib

English

From a covariant structure with < we obtain a covariant structure with ≤: CovariantClass M N μ (≤).

Русский

Из ковариантности по < следует ковариантность по ≤.

LaTeX

$$$\langle CovariantClass\, M\, N\, μ\, (<) \rangle \Rightarrow CovariantClass\, M\, N\, μ\, (\le)$$$

Lean4

theorem covariantClass_le_of_lt [PartialOrder N] [CovariantClass M N μ (· < ·)] : CovariantClass M N μ (· ≤ ·) :=
  ⟨covariant_le_of_covariant_lt _ _ _ CovariantClass.elim⟩

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