Theorems · Theorem · order theory
Set.Finite.preimage
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set β}, Set.InjOn f (f ⁻¹' s) → s.Finite → (f ⁻¹' s).Finite- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.preimagestatement and proof · cited by 4,946
- Set.Finitestatement and proof · cited by 1,814
- Set.InjOnstatement and proof · cited by 543
- Set.Finite.subsetproof · cited by 285
- Set.image_preimage_subsetproof · cited by 75
- Set.Finite.of_finite_imageproof · cited by 20
Cited by16
Results whose statement or proof uses this declaration.
- Function.Injective.tendsto_cofiniteproof · cited by 9
- AddMonoidHom.map_finsumproof · cited by 9
- Function.Injective.tprod_eqproof · cited by 6
- Function.Injective.tsum_eqproof · cited by 6
- MonoidHom.map_finprodproof · cited by 4
- Set.Finite.preimage_embeddingproof · cited by 2
- AlgebraicGeometry.LocallyQuasiFinite.of_finite_preimage_singletonproof · cited by 2
- FormalMultilinearSeries.changeOrigin_eval_of_finiteproof · cited by 1
- IsCountablyCompact.exists_accPt_of_infiniteproof · cited by 1
- IsLinearSet.exists_fg_eq_subtypeValproof · cited by 1
- LocallyFinite.comp_injOnproof · cited by 1
- FirstOrder.Language.Substructure.FG.of_map_embeddingproof · cited by 1