Theorems · Theorem · general topology

ContinuousMap.idealOpensGI_choice

∀ (X : Type u_1) (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [inst_2 : CompactSpace X]
  [inst_3 : T2Space X] (I : Ideal C(X, 𝕜)) (x : ContinuousMap.idealOfSet 𝕜 ↑(ContinuousMap.opensOfIdeal I) ≤ I),
  (ContinuousMap.idealOpensGI X 𝕜).choice I x = ContinuousMap.opensOfIdeal I.closure

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeTopologicalSpaceCompactSpaceT2Space