List

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

Statistics

Metric	Count
Definitions	0
Theorems canLift, range_list_get, range_list_getD, range_list_getElem?, range_list_getI, range_list_map, range_list_map_coe	7
Total	7

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift	—	Set.mem_range Set.range_list_map CanLift.prf

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_list_get 📖	mathematical	—	range setOf	—	ext mem_setOf_eq mem_range
range_list_getD 📖	mathematical	—	range Set instInsert setOf	—	image_congr range_list_getElem? image_insert_eq image_image image_id'
range_list_getElem? 📖	mathematical	—	range Set instInsert image setOf	—	range_list_get range_comp HasSubset.Subset.antisymm instAntisymmSubset range_subset_iff le_or_gt insert_subset_iff le_rfl
range_list_getI 📖	mathematical	—	range List.getI Set instInsert setOf	—	range_list_getD
range_list_map 📖	mathematical	—	range setOf	—	antisymm instAntisymmSubset range_subset_iff mem_range_self
range_list_map_coe 📖	mathematical	—	range Set instMembership setOf	—	range_list_map Subtype.range_coe

---

← Back to Index