Lemmas

Statistics

Metric	Count
Definitions	0
Theorems `coe_finset_sup`, `coe_indicator`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finset_sup` 📖	mathematical	—	`ofNNReal` `Finset.sup` `NNReal` `instSemilatticeSupNNReal` `NNReal.instOrderBot` `ENNReal` `instSemilatticeSupENNReal` `instOrderBot`	—	`Finset.comp_sup_eq_sup_comp_of_is_total` `coe_mono`
`coe_indicator` 📖	mathematical	—	`ofNNReal` `Set.indicator` `NNReal` `instZeroNNReal` `ENNReal` `instZeroENNReal`	—	`map_indicator` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

---