le_mulIndicator — Mathlib

English

For any s, f, a, mulIndicator s f a ≤ 1 if f(a) ≤ 1 for all a ∈ s.

Русский

Для любого s, f, a, mulIndicator s f a ≤ 1 при условии f(a) ≤ 1 для всех a ∈ s.

LaTeX

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

Lean4

@[to_additive]
theorem le_mulIndicator (hfg : ∀ a ∈ s, f a ≤ g a) (hf : ∀ a ∉ s, f a ≤ 1) : f ≤ mulIndicator s g := fun _ ↦
  le_mulIndicator_apply (hfg _) (hf _)

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