Theorems · Theorem · combinatorics
Pi.infinite_of_exists_right
∀ {ι : Sort u_4} {π : ι → Sort u_5} (i : ι) [Infinite (π i)] [∀ (i : ι), Nonempty (π i)], Infinite ((i : ι) → π i)If at least one π i is infinite and the rest nonempty, the pi type of all π is infinite.
- Defined in
- Mathlib.Data.Fintype.Prod
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.updateproof · cited by 502
- Infinitestatement and proof · cited by 352
- Infinite.of_injectiveproof · cited by 10
- Function.update_injectiveproof · cited by 8
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.