Theorems · Theorem · general topology

ContinuousMap.induction_on_of_compact

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [CompactSpace ↑s] {p : C(↑s, 𝕜) → Prop},
  (∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) →
    p (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) →
      p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) →
        (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) →
          (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) →
            (∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in nhds f, p g) → p f) → ∀ (f : C(↑s, 𝕜)), p f

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeCompactSpace