English
The Lie span induction principle: if a property p holds for 0, every element of s, is preserved under addition, scalar multiplication and Lie bracket, then p holds for all elements of lieSpan_R L s.
Русский
Применение индукции по порождению Ли: если свойство p справедливо для 0, для каждого элемента из s и сохраняется при сложении, умножении на скаляры и взятии скобки, то оно верно и для всех элементов lieSpan_R L s.
LaTeX
$$([elab_as_elim] lieSpan_induction)$$
Lean4
/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition, scalar multiplication and the Lie bracket, then `p` holds for all
elements of the Lie algebra spanned by `s`. -/
@[elab_as_elim]
theorem lieSpan_induction {p : (x : L) → x ∈ lieSpan R L s → Prop} (mem : ∀ (x) (h : x ∈ s), p x (subset_lieSpan h))
(zero : p 0 (LieSubalgebra.zero_mem _))
(add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (LieSubalgebra.add_mem _ ‹_› ‹_›))
(smul : ∀ (a : R) (x hx), p x hx → p (a • x) (LieSubalgebra.smul_mem _ _ ‹_›)) {x}
(lie : ∀ x y hx hy, p x hx → p y hy → p (⁅x, y⁆) (LieSubalgebra.lie_mem _ ‹_› ‹_›)) (hx : x ∈ lieSpan R L s) :
p x hx :=
by
let p : LieSubalgebra R L :=
{ carrier := {x | ∃ hx, p x hx}
add_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, add _ _ _ _ hpx hpy⟩
zero_mem' := ⟨_, zero⟩
smul_mem' := fun r ↦ fun ⟨_, hpx⟩ ↦ ⟨_, smul r _ _ hpx⟩
lie_mem' := fun ⟨_, hpx⟩ ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ _ hpx hpy⟩ }
exact lieSpan_le (K := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id
