Set

📁 Source: Mathlib/Data/Finite/Set.lean

Statistics

Metric	Count
Definitions	0
Theorems finite_of_finite_image, of_injective_finite_range	2
Total	2

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_injective_finite_range 📖	mathematical	—	Finite	—	of_injective Function.Injective.codRestrict Set.mem_range_self

Finite.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_finite_image 📖	mathematical	Set.InjOn	Finite Set.Elem	—	Finite.of_equiv Set.BijOn.mapsTo Set.InjOn.bijOn_image Set.BijOn.bijective

---

← Back to Index