Theorem IsInducing.topologicalKrullDim_le

Modification history

2026-06-22 16:23
Mathlib/Topology/KrullDimension.lean
chore(Topology): namespace lemmas around `IsInducing`, `IsQuotientMap` etc (#40891) …
Deleted IsInducing.topologicalKrullDim_leView on Github →
2025-11-03 14:11
Mathlib/Topology/KrullDimension.lean
feat(Topology/KrullDimension): add subspace dimension inequality (#29728) …
Added IsInducing.topologicalKrullDim_leView on Github →