Theorems · Theorem · group theory

AddSubmonoid.dense_induction

∀ {M : Type u_1} [inst : AddZeroClass M] {motive : M → Prop} (s : Set M),
  AddSubmonoid.closure s = ⊤ →
    (∀ x ∈ s, motive x) → motive 0 → (∀ (x y : M), motive x → motive y → motive (x + y)) → ∀ (x : M), motive x

If s is a dense set in an additive monoid M, AddSubmonoid.closure s = ⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s, verify p 0, and verify that p x and p y imply p (x + y).

Defined in

Mathlib.Algebra.Group.Submonoid.Basic

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddZeroClass