Theorems · Theorem · group theory

Submonoid.dense_induction

∀ {M : Type u_1} [inst : MulOneClass M] {motive : M → Prop} (s : Set M),
  Submonoid.closure s = ⊤ →
    (∀ x ∈ s, motive x) → motive 1 → (∀ (x y : M), motive x → motive y → motive (x * y)) → ∀ (x : M), motive x

If s is a dense set in a monoid M, Submonoid.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 1, 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

MulOneClass