FunOnFinite

Statistics

Metric	Count
Definitions	0
Theorems `continuous_linearMap`, `continuous_map`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_linearMap` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `LinearMap.instFunLike` `linearMap`	—	`continuous_map`
`continuous_map` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `map`	—	`continuous_pi` `Finite.of_fintype` `map_apply_apply` `continuous_finset_sum` `continuous_apply`

---