KrullDimension

📁 Source: Mathlib/Topology/KrullDimension.lean

Statistics

Metric	Count
Definitions topologicalKrullDim	1
Theorems topologicalKrullDim_le, topologicalKrullDim_eq, topologicalKrullDim_le, topologicalKrullDim_subspace_le, topologicalKrullDim_zero_of_discreteTopology	5
Total	6

IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalKrullDim_le 📖	mathematical	Topology.IsInducing	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat topologicalKrullDim	—	IsInducing.topologicalKrullDim_le

IsHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalKrullDim_eq 📖	mathematical	IsHomeomorph	topologicalKrullDim	—	IsInducing.topologicalKrullDim_le Topology.IsEmbedding.toIsInducing Topology.IsClosedEmbedding.toIsEmbedding isClosedEmbedding Homeomorph.isClosedEmbedding le_antisymm

IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalKrullDim_le 📖	mathematical	Topology.IsInducing	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat topologicalKrullDim	—	Order.krullDim_le_of_strictMono Topology.IsInducing.continuous TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing

(root)

Definitions

Name	Category	Theorems
topologicalKrullDim 📖	CompOp	6 math math: topologicalKrullDim_subspace_le, topologicalKrullDim_zero_of_discreteTopology, IsInducing.topologicalKrullDim_le, IsClosedEmbedding.topologicalKrullDim_le, PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim, IsHomeomorph.topologicalKrullDim_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
topologicalKrullDim_subspace_le 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat topologicalKrullDim Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	IsInducing.topologicalKrullDim_le Topology.IsInducing.subtypeVal
topologicalKrullDim_zero_of_discreteTopology 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat topologicalKrullDim WithBot.zero instZeroENat	—	Order.krullDim_nonpos_iff_forall_isMax Eq.le LE.le.antisymm' IsIrreducible.nonempty TopologicalSpace.IrreducibleCloseds.isIrreducible' IsDiscrete.subsingleton_of_isPreirreducible DiscreteTopology.isDiscrete instDiscreteTopologySubtype IsIrreducible.isPreirreducible

---

← Back to Index