mulIndicator_apply_le_one

Mathlib.Algebra.Order.Group.Indicator

URI: https://scilib.ai/kg/mathlib#Set.mulIndicator_apply_le_one

English

For any h: a ∈ s → f(a) ≤ 1, we have mulIndicator s f a ≤ 1.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mulIndicator_apply_le_one (h : a ∈ s → f a ≤ 1) : mulIndicator s f a ≤ 1 :=
  mulIndicator_apply_le' h fun _ ↦ le_rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru