indicator_le_indicator_nonneg — Mathlib

English

For any s and f, the indicator of f on s is bounded above by the indicator of f on the nonnegative set {a | 0 ≤ f a}.

Русский

Для любых множества s и функции f указатель f на s не превосходит указатель f на множество, состоящее из точек, где f(a) неотрицательно.

LaTeX

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

Lean4

theorem indicator_le_indicator_nonneg (s : Set α) (f : α → M) : s.indicator f ≤ {a | 0 ≤ f a}.indicator f :=
  by
  intro a
  classical
  simp_rw [indicator_apply]
  split_ifs
  exacts [le_rfl, (not_le.1 ‹_›).le, ‹_›, le_rfl]

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