induction_on — Mathlib

English

Induction on quotient elements: to prove a property for all x in α / s, it suffices to prove it for all representatives in α.

Русский

Индукция по элементам фактор-группы: чтобы доказать свойство для всех x в α / s, достаточно доказать для всех представителей в α.

LaTeX

$$induction_on : {C : α / s → Prop} → (∀ z, C (QuotientGroup.mk z)) → ∀ x, C x$$

Lean4

@[to_additive (attr := elab_as_elim)]
theorem induction_on {C : α ⧸ s → Prop} (x : α ⧸ s) (H : ∀ z, C (QuotientGroup.mk z)) : C x :=
  Quotient.inductionOn' x H

Похожие утверждения