English
An induction principle for lieSpan 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 every element of lieSpan(R,L,s).
Русский
Принцип индукции для принадлежности lieSpan: если верно p(0) и для всех элементов s, и p сохраняется при сложении, умножении на скаляр и скобке Ли, то p верно для каждого элемента lieSpan(R,L,s).
LaTeX
$$\\forall p:(x:M)\\to p\\;x\\;\\text{ oxide}, \\ldots$$
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 submodule spanned by `s`. -/
@[elab_as_elim]
theorem lieSpan_induction {p : (x : M) → x ∈ lieSpan R L s → Prop} (mem : ∀ (x) (h : x ∈ s), p x (subset_lieSpan h))
(zero : p 0 (LieSubmodule.zero_mem _)) (add : ∀ x y hx hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›))
(smul : ∀ (a : R) (x hx), p x hx → p (a • x) (SMulMemClass.smul_mem _ hx)) {x}
(lie : ∀ (x : L) (y hy), p y hy → p (⁅x, y⁆) (LieSubmodule.lie_mem _ ‹_›)) (hx : x ∈ lieSpan R L s) : p x hx :=
by
let p : LieSubmodule R L M :=
{ 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 ⟨_, hpy⟩ ↦ ⟨_, lie _ _ _ hpy⟩ }
exact lieSpan_le (N := p) |>.mpr (fun y hy ↦ ⟨subset_lieSpan hy, mem y hy⟩) hx |>.elim fun _ ↦ id
