English
A standard induction principle for M ∗ N: if a property holds for left injections and for right injections and is closed under multiplication, then it holds for all elements.
Русский
Стандартный принцип индукции по M ∗ N: если свойство верно для левых внедрений и правых внедрений и сохраняется при умножении, то верно для всех элементов.
LaTeX
$$$\forall C:(M\ast N)\to\mathrm{Prop},\; (\forall m, C(inl m)) \to (\forall n, C(inr n)) \to (\forall x y, C(x) \to C(y) \to C(x\,y)) \to C(m).$$$
Lean4
@[to_additive (attr := elab_as_elim)]
theorem induction_on {C : M ∗ N → Prop} (m : M ∗ N) (inl : ∀ m, C (inl m)) (inr : ∀ n, C (inr n))
(mul : ∀ x y, C x → C y → C (x * y)) : C m :=
induction_on' m (by simpa using inl 1) (fun _ _ ↦ mul _ _ (inl _)) fun _ _ ↦ mul _ _ (inr _)
