one_le_mulIndicator_apply — Mathlib

English

If h maps a ∈ s to f(a) ≤ g(a), then mulIndicator s f ≤ mulIndicator s g.

Русский

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

LaTeX

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

Lean4

@[to_additive indicator_apply_nonneg]
theorem one_le_mulIndicator_apply (h : a ∈ s → 1 ≤ f a) : 1 ≤ mulIndicator s f a :=
  le_mulIndicator_apply h fun _ ↦ le_rfl

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