Theorems · Theorem · group theory

Subgroup.closure_induction

∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : (g : G) → g ∈ Subgroup.closure k → Prop},
  (∀ (x : G) (hx : x ∈ k), p x ⋯) →
    p 1 ⋯ →
      (∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) →
        (∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) → ∀ {x : G} (hx : x ∈ Subgroup.closure k), p x hx

An induction principle for closure membership. If p holds for 1 and all elements of k, and is preserved under multiplication and inverse, then p holds for all elements of the closure of k. See also Subgroup.closure_induction_left and Subgroup.closure_induction_right for versions that only require showing p is preserved by multiplication by elements in k.

Defined in

Mathlib.Algebra.Group.Subgroup.Lattice

Cited by

14 results in Mathlib

Foundations

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

Assumes

Group