Theorems · Theorem · combinatorics
Set.forall_finite_image_eval_iff
∀ {δ : Type u_3} [Finite δ] {κ : δ → Type u_4} {s : Set ((d : δ) → κ d)},
(∀ (d : δ), (Function.eval d '' s).Finite) ↔ s.Finite- Defined in
- Mathlib.Data.Fintype.Pi
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Finite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.imagestatement and proof · cited by 5,609
- Set.univproof · cited by 3,945
- Finitestatement and proof · cited by 3,029
- Set.Finitestatement and proof · cited by 1,814
- Set.Finite.subsetproof · cited by 285
- Function.evalstatement and proof · cited by 140
- Set.Finite.imageproof · cited by 96
- Set.subset_pi_eval_imageproof · cited by 5
- Set.Finite.piproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.