mulIndicator_le_one

Mathlib.Algebra.Order.Group.Indicator

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

English

For any s, f, a, mulIndicator s f a ≤ 1 if f(a) ≤ 1 when 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 mulIndicator_le_one (h : ∀ a ∈ s, f a ≤ 1) (a : α) : mulIndicator s f a ≤ 1 :=
  mulIndicator_apply_le_one (h a)

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

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

Разделы

Аффилиация

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