English
An induction principle for C(s, k): if a property holds for constants, id, star-id, closed under addition, multiplication, scaling, and is preserved under adjoin and closure, then it holds for all functions in C(s, k).
Русский
Принцип индукции по пространству C(s, k): если свойство выполняется для констант, идента, звездного идента, замкнуто по сложению, умножению, масштабированию, сохраняется под адъойн и замыкание, то выполняется для всех функций в C(s, k).
LaTeX
$$$\text{InductionOn}(s, \mathbb{K})$$$
Lean4
/-- An induction principle for `C(s, 𝕜)`. -/
@[elab_as_elim]
theorem induction_on {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜} {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)) (closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ f, p f)
(f : C(s, 𝕜)) : p f := by
refine closure (fun f hf => ?_) f
rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf
induction hf using Algebra.adjoin_induction with
| mem f hf =>
simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf
rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
obtain (rfl | rfl) := hf
all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
| algebraMap r => exact const r
| add _ _ _ _ hf hg => exact add _ _ hf hg
| mul _ _ _ _ hf hg => exact mul _ _ hf hg
