mulIndicator_le_mulIndicator_of_subset

English

If s ⊆ t and 1 ≤ f holds for all x (i.e., 1 ≤ f x for every x), then mulIndicator s f ≤ mulIndicator t f as functions.

Русский

Если s ⊆ t и выполняется 1 ≤ f(x) для всех x, то mulIndicator s f ≤ mulIndicator t f как функции.

LaTeX

$$$s \subseteq t \land (\forall x, 1 \le f x) \Rightarrow (\forall a, mulIndicator\, s\, f\, a \le mulIndicator\, t\, f\, a)$$$

Lean4

@[to_additive]
theorem mulIndicator_le_mulIndicator_of_subset (h : s ⊆ t) (hf : 1 ≤ f) : mulIndicator s f ≤ mulIndicator t f := fun _ ↦
  mulIndicator_le_mulIndicator_apply_of_subset h (hf _)

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