Theorems · Theorem · general topology

Topology.IsInducing.topologicalKrullDim_le

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : Y → X},
  Topology.IsInducing f → topologicalKrullDim Y ≤ topologicalKrullDim X

If f : Y → X is inducing, then dim(Y) ≤ dim(X).

Defined in

Mathlib.Topology.KrullDimension

Cited by

2 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace