Theorems · Theorem · logic and foundations
Quotient.induction_on_pi
∀ {ι : Type u_3} {α : ι → Sort u_4} {s : (i : ι) → Setoid (α i)} {p : ((i : ι) → Quotient (s i)) → Prop}
(f : (i : ι) → Quotient (s i)), (∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧) → p f- Defined in
- Mathlib.Data.Quot
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quotient.outproof · cited by 141
- Quotient.out_eqproof · cited by 27
Cited by3
Results whose statement or proof uses this declaration.
- Cardinal.induction_on_piproof · cited by 1
- Path.Homotopic.comp_pi_eq_pi_compproof · cited by 0
- Path.Homotopic.proj_piproof · cited by 0