English
Induction principle for C(s, k) with a compact s; similar to prior induction but in the complex/real-valued map setting.
Русский
Индукционный принцип для C(s, k) в случае компактного s; аналогично предыдущей индукции, но в пространстве вещественных/комплексных отображений.
LaTeX
$$$\text{InductionOnOfCompact}(s, \mathbb{K})$$$
Lean4
/-- An induction principle for `C(s, 𝕜)₀`. -/
@[elab_as_elim]
theorem induction_on {s : Set 𝕜} [Fact (0 ∈ 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)) (closure : (∀ f ∈ adjoin 𝕜 {(.id s : C(s, 𝕜)₀)}, p f) → ∀ f, p f)
(f : C(s, 𝕜)₀) : p f := by
refine closure (fun f hf => ?_) f
induction hf using NonUnitalAlgebra.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 assumption
| zero => exact zero
| add _ _ _ _ hf hg => exact add _ _ hf hg
| mul _ _ _ _ hf hg => exact mul _ _ hf hg
| smul _ _ _ hf => exact smul _ _ hf
