English
Variant of the induction principle for C(s, k)₀ on compact s; the result follows similarly by density of adjoin id.
Русский
Вариант принципа индукции для C(s, k)₀ на компактном s; результат следует из плотности ограниченного идентитета.
LaTeX
$$$\text{InductionOnOfCompact}(s, \mathbb{K})$$$
Lean4
@[elab_as_elim]
theorem induction_on_of_compact {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜} [CompactSpace s] {p : C(s, 𝕜) → Prop}
(const : ∀ r, p (.const s r)) (id : p (.restrict s <| .id 𝕜)) (star_id : p (star (.restrict s <| .id 𝕜)))
(add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
(frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)) : p f :=
by
refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_
have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)
rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this
exact this.mp <| .of_forall h
