mulIndicator_le_mulIndicator — Mathlib

English

If f ≤ g pointwise, then s.mulIndicator f ≤ s.mulIndicator g pointwise.

Русский

Если f ≤ g по всем аргументам, то s.mulIndicator f ≤ s.mulIndicator g по всем аргументам.

LaTeX

$$$\\forall f,g:\\ α \\to M, \\ f \\le g \\Rightarrow s.mulIndicator f \\le s.mulIndicator g.$$$

Lean4

@[to_additive (attr := mono, gcongr)]
theorem mulIndicator_le_mulIndicator (h : f a ≤ g a) : mulIndicator s f a ≤ mulIndicator s g a :=
  mulIndicator_rel_mulIndicator le_rfl fun _ ↦ h

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