covariant_div — Mathlib

English

Let α be a type with a division operation. For filters on α, the pointwise division is monotone in the left argument with respect to the filter order: if f ≤ f' then f / h ≤ f' / h for every filter h on α.

Русский

Пусть α — множество с операцией деления. Для фильтров над α точечное деление является монотонным по левому аргументу относительно порядка фильтров: если f ≤ f', то f / h ≤ f' / h для любого фильтра h над α.

LaTeX

$$$\forall f,g,h \in \mathrm{Filter}(\alpha),\ f \le g \Rightarrow f / h \le g / h.$$$

Lean4

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

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