mulLeftMono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance mulLeftMono : MulLeftMono (Filter α) :=
  ⟨fun _ _ _ => map₂_mono_left⟩

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