mulIndicator_apply_le' — Mathlib

English

If hfg ensures a ∈ s implies f(a) ≤ y and hg ensures a ∉ s implies 1 ≤ y, then mulIndicator s f a ≤ y.

Русский

Если для всех a: если a ∈ s, то f(a) ≤ y, и если a ∉ s, то 1 ≤ y, тогда mulIndicator s f a ≤ y.

LaTeX

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

Lean4

@[to_additive]
theorem mulIndicator_apply_le' (hfg : a ∈ s → f a ≤ y) (hg : a ∉ s → 1 ≤ y) : mulIndicator s f a ≤ y :=
  by
  by_cases ha : a ∈ s
  · simpa [ha] using hfg ha
  · simpa [ha] using hg ha

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