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 _ _ _