Theorems · Theorem · general topology

ContinuousMapZero.induction_on_of_compact

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [inst_1 : Fact (0 ∈ s)] [CompactSpace ↑s]
  {p : ContinuousMapZero (↑s) 𝕜 → Prop},
  p 0 →
    p (ContinuousMapZero.id s) →
      p (star (ContinuousMapZero.id s)) →
        (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f + g)) →
          (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f * g)) →
            (∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p f → p (r • f)) →
              (∀ (f : ContinuousMapZero (↑s) 𝕜), (∃ᶠ (g : ContinuousMapZero (↑s) 𝕜) in nhds f, p g) → p f) →
                ∀ (f : ContinuousMapZero (↑s) 𝕜), p f

Defined in

Mathlib.Topology.ContinuousMap.StoneWeierstrass

Cited by

4 results in Mathlib

Foundations

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

Assumes

RCLikeFactCompactSpace