indicator_nonpos_le_indicator — Mathlib

English

For sets s and function f in a linear ordered group, the indicator of nonpositive values is bounded above by the indicator on s: {a | f a ≤ 0}.indicator f ≤ s.indicator f.

Русский

Для множества s и функции f в линейно упорядоченной группе величина индикатора неотрицательных значений ограничивает индикатор на s: {a | f(a) ≤ 0}.indicator f ≤ s.indicator f.

LaTeX

$$${a| f a \le 0}.indicator f \le s.indicator f$$$

Lean4

theorem indicator_nonpos_le_indicator (s : Set α) (f : α → M) : {a | f a ≤ 0}.indicator f ≤ s.indicator f :=
  indicator_le_indicator_nonneg (M := Mᵒᵈ) _ _

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