coe_indicator — Mathlib

English

For any set s ⊆ A, function f: A → ℚ≥0, and a ∈ A, the value of s.indicator f at a, mapped to ℚ, equals s.indicator of (f(a)) viewed in ℚ.

Русский

Для множества s ⊆ A, функции f: A → ℚ≥0 и элемента a ∈ A верно: ((s.indicator f a) : ℚ) = s.indicator (fun x ↦ f x) a.

LaTeX

$$$\big((s.indicator f a) : \mathbb{Q}\big) = s.indicator (\lambda x. f x) a$$$

Lean4

@[simp, norm_cast]
theorem coe_indicator (s : Set α) (f : α → ℚ≥0) (a : α) :
    ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (fun x ↦ ↑(f x)) a :=
  (coeHom : ℚ≥0 →+ ℚ).map_indicator _ _ _

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