mulIndicator_mono — Mathlib

English

If f ≤ g then s.mulIndicator f ≤ s.mulIndicator g; this is a monotone property compatible with gcongr.

Русский

Если f ≤ g, то s.mulIndicator f ≤ s.mulIndicator g; данное свойство монотонно совместимо с gcongr.

LaTeX

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

Lean4

@[to_additive (attr := gcongr)]
theorem mulIndicator_mono (h : f ≤ g) : s.mulIndicator f ≤ s.mulIndicator g := fun _ ↦
  mulIndicator_le_mulIndicator (h _)

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