mulIndicator_le' — Mathlib

English

If for all a ∈ s we have f(a) ≤ g(a) and for a ∉ s we have 1 ≤ g(a), then mulIndicator s f ≤ g.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mulIndicator_le' (hfg : ∀ a ∈ s, f a ≤ g a) (hg : ∀ a, a ∉ s → 1 ≤ g a) : mulIndicator s f ≤ g := fun _ ↦
  mulIndicator_apply_le' (hfg _) (hg _)

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