mulIndicator_le_mulIndicator' — Mathlib

English

If h(a) ≤ g(a) for all a, then mulIndicator s f ≤ mulIndicator s g.

Русский

Если h(a) ≤ g(a) для всех a, то mulIndicator s f ≤ mulIndicator s g.

LaTeX

$$$\\forall a, (a \\in s \\Rightarrow f(a) \\le g(a)) \\Rightarrow \\mathrm{mulIndicator}(s,f)(a) \\le \\mathrm{mulIndicator}(s,g)(a).$$$

Lean4

@[to_additive]
theorem mulIndicator_le_mulIndicator' (h : a ∈ s → f a ≤ g a) : mulIndicator s f a ≤ mulIndicator s g a :=
  mulIndicator_rel_mulIndicator le_rfl h

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