English
Induction principle: to prove a property P for all elements of s • N, it suffices to verify P on r • n for all r ∈ s and n ∈ N, to verify closure under multiplying by any r ∈ R, under addition, and to check P(0).
Русский
Принцип индукции: чтобы доказать свойство P для всех элементов s • N, достаточно проверить P на выражениях r • n с r ∈ s и n ∈ N, проверить замкнутость относительно умножения на произвольный r ∈ R, по сложению и получить P(0).
LaTeX
$$$\forall x\,(x \in s \cdot N) \Rightarrow P(x) \quad\text{provided that:}$ \\ P(r \cdot n) \text{ for all } r \in s, n \in N, \\ P(m) \implies P(r \cdot m) \text{ for all } r \in R, m \in s \cdot N, \\ P(m_1), P(m_2) \Rightarrow P(m_1 + m_2), \\ P(0).$$$$
Lean4
/-- Induction principle for set acting on submodules. To prove `P` holds for all `s • N`, it is enough
to prove:
- for all `r ∈ s` and `n ∈ N`, `P (r • n)`;
- for all `r` and `m ∈ s • N`, `P (r • n)`;
- for all `m₁, m₂`, `P m₁` and `P m₂` implies `P (m₁ + m₂)`;
- `P 0`.
To invoke this induction principle, use `induction x, hx using Submodule.set_smul_inductionOn` where
`x : M` and `hx : x ∈ s • N`
-/
@[elab_as_elim]
theorem set_smul_inductionOn {motive : (x : M) → (_ : x ∈ s • N) → Prop} (x : M) (hx : x ∈ s • N)
(smul₀ : ∀ ⦃r : S⦄ ⦃n : M⦄ (mem₁ : r ∈ s) (mem₂ : n ∈ N), motive (r • n) (mem_set_smul_of_mem_mem mem₁ mem₂))
(smul₁ : ∀ (r : R) ⦃m : M⦄ (mem : m ∈ s • N), motive m mem → motive (r • m) (Submodule.smul_mem _ r mem)) --
(add :
∀ ⦃m₁ m₂ : M⦄ (mem₁ : m₁ ∈ s • N) (mem₂ : m₂ ∈ s • N),
motive m₁ mem₁ → motive m₂ mem₂ → motive (m₁ + m₂) (Submodule.add_mem _ mem₁ mem₂))
(zero : motive 0 (Submodule.zero_mem _)) : motive x hx :=
let ⟨_, h⟩ :=
set_smul_le s N
{ carrier := {m | ∃ (mem : m ∈ s • N), motive m mem}, zero_mem' := ⟨Submodule.zero_mem _, zero⟩
add_mem' := fun ⟨mem, h⟩ ⟨mem', h'⟩ ↦ ⟨_, add mem mem' h h'⟩
smul_mem' := fun r _ ⟨mem, h⟩ ↦ ⟨_, smul₁ r mem h⟩ }
(fun _ _ mem mem' ↦ ⟨mem_set_smul_of_mem_mem mem mem', smul₀ mem mem'⟩) hx
h
