English
Induction principle for the non-unital setting C(s, k)₀ on compact s; mirrors the unital version.
Русский
Индукционный принцип для неразделенной подалгебры C(s, k)₀ на компактном s; повторяет единичную версию.
LaTeX
$$$\text{InductionOnOfCompact}(s)\text{ in non-unital setting}$$$
Lean4
@[elab_as_elim]
theorem induction_on_of_compact {s : Set 𝕜} [Fact (0 ∈ s)] [CompactSpace s] {p : C(s, 𝕜)₀ → Prop} (zero : p 0)
(id : p (.id s)) (star_id : p (star (.id s))) (add : ∀ f g, p f → p g → p (f + g))
(mul : ∀ f g, p f → p g → p (f * g)) (smul : ∀ (r : 𝕜) f, p f → p (r • f))
(frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)₀) : p f :=
by
refine f.induction_on zero id star_id add mul smul fun h f ↦ frequently f ?_
have := (ContinuousMapZero.adjoin_id_dense s).closure_eq ▸ Set.mem_univ (x := f)
exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h
