covariant_smul_filter — Mathlib

English

The scalar action on filters is covariant: the map f ↦ a • f is order-preserving.

Русский

Действие скаляра на фильтры ковариантно: отображение f ↦ a • f сохраняет порядок.

LaTeX

$$$\text{CovariantClass }\, a: f \mapsto a \cdot f$ is monotone in $f$, i.e., $f_1 \le f_2 \Rightarrow a \cdot f_1 \le a \cdot f_2$$$

Lean4

@[to_additive]
instance covariant_smul_filter : CovariantClass α (Filter β) (· • ·) (· ≤ ·) :=
  ⟨fun _ => @map_mono β β _⟩

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