Documentation Verification Report

Indicator

📁 Source: Mathlib/Data/Finsupp/Indicator.lean

Statistics

Metric	Count
Definitions `indicator`	1
Theorems `indicator_apply`, `indicator_injective`, `indicator_of_mem`, `indicator_of_notMem`, `single_eq_indicator`, `support_indicator_subset`	6
Total	7

Finsupp

Definitions

Name	Category	Theorems
`indicator` 📖	CompOp	12 math math: `sum_indicator_index`, `sum_indicator_index_eq_sum_attach`, `single_eq_indicator`, `indicator_of_notMem`, `indicator_apply`, `prod_indicator_index_eq_prod_attach`, `prod_indicator_index`, `indicator_eq_sum_attach_single`, `indicator_eq_sum_single`, `indicator_of_mem`, `support_indicator_subset`, `indicator_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indicator_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `indicator` `Finset` `Finset.instMembership` `Finset.decidableMem`	—	—
`indicator_injective` 📖	mathematical	—	`Finsupp` `indicator`	—	`indicator_of_mem` `DFunLike.congr_fun`
`indicator_of_mem` 📖	mathematical	`Finset` `Finset.instMembership`	`DFunLike.coe` `Finsupp` `instFunLike` `indicator`	—	—
`indicator_of_notMem` 📖	mathematical	`Finset` `Finset.instMembership`	`DFunLike.coe` `Finsupp` `instFunLike` `indicator`	—	—
`single_eq_indicator` 📖	mathematical	—	`single` `indicator` `Finset` `Finset.instSingleton`	—	`ext` `single_apply` `indicator_apply`
`support_indicator_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `indicator`	—	`mem_support_iff` `Finset.mem_coe` `indicator_of_notMem`

---

← Back to Index