covariant_smul — Mathlib

English

There is a covariant class structure for the operation with respect to the order; in particular the operation is monotone in the left argument (as an instance).

Русский

Существуют требования к ковариантности операции относительно порядка: она монотонна по левому аргументу (как инстанс).

LaTeX

$$CovariantClass(Filter α)(Filter β)(fun x1 x2 => x1 x2) (fun x1 x2 => x1 ≤ x2)$$

Lean4

@[to_additive]
instance covariant_smul : CovariantClass (Filter α) (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ _ _ => map₂_mono_left⟩

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