Theorem ContinuousMapZero.induction_on_of_compact

Modification history

2025-09-18 15:32
Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
refactor: switch to using `Fact (0 ∈ s)` for `ContinuousMapZero.id` (#29563) …
Modified ContinuousMapZero.induction_on_of_compactView on Github →
2024-10-20 13:19
Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
feat: induction principles for ContinuousMap via Stone-Weierstrass (#17831) …
Added ContinuousMapZero.induction_on_of_compactView on Github →