Range

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

Statistics

Metric	Count
Definitions fintypeRange	1
Theorems finite_range, finite_replacement, dependent_image, exists_subset_finite_image_eq, finite_range	5
Total	6

Finite.Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_range 📖	mathematical	—	Finite Set.Elem Set.range	—	Finite.of_fintype instFinitePLift
finite_replacement 📖	mathematical	—	Finite Set.Elem setOf	—	finite_range

Set

Definitions

Name	Category	Theorems
fintypeRange 📖	CompOp	2 math math: LinearMap.toMatrix_reindexRange, LinearMap.toMatrixAlgEquiv_reindexRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_range 📖	mathematical	—	Finite range	—	toFinite Finite.Set.finite_range

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependent_image 📖	mathematical	—	Set.Finite setOf Set Set.instMembership	—	to_subtype Set.finite_range
exists_subset_finite_image_eq 📖	mathematical	Set Set.instHasSubset Set.image	Set Set.instHasSubset Set.Finite Set.image	—	to_subtype Set.finite_range Set.ext

---

← Back to Index