le_mulIndicator_apply — Mathlib

English

For any a, if for all a ∈ s we have f(a) ≤ g(a) and for a ∉ s we have 1 ≤ y, then y ≤ mulIndicator s g a.

Русский

Для любого a, если для всех a в s выполняется f(a) ≤ g(a) и для a не в s выполняется 1 ≤ y, тогда y ≤ mulIndicator s g a.

LaTeX

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

Lean4

@[to_additive]
theorem le_mulIndicator_apply (hfg : a ∈ s → y ≤ g a) (hf : a ∉ s → y ≤ 1) : y ≤ mulIndicator s g a :=
  mulIndicator_apply_le' (M := Mᵒᵈ) hfg hf

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