mulRightMono — Mathlib

English

Let α be a type with a multiplication. The multiplication of filters is monotone in the right argument: for any filters f and g, g' on α, if g ≤ g', then f * g ≤ f * g'.

Русский

Пусть α — множество с операцией умножения. Умножение фильтров по правому аргументу монотонно: для любых фильтров f и g, g' на α, если g ≤ g', то f * g ≤ f * g'.

LaTeX

$$$\\forall f,g,g' \\; (g \\le g') \\Rightarrow (f * g \\le f * g').$$$

Lean4

@[to_additive]
instance mulRightMono : MulRightMono (Filter α) :=
  ⟨fun _ _ _ => map₂_mono_right⟩

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