Theorems · Theorem · general topology

ContinuousMap.ideal_isMaximal_iff

∀ {X : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  (I : Ideal C(X, 𝕜)) [hI : IsClosed ↑I], I.IsMaximal ↔ ∃ x, ContinuousMap.idealOfSet 𝕜 {x}ᶜ = I

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpaceCompactSpaceT2SpaceIsClosed