UniqueChoice

📁 Source: SDG/Axiom/UniqueChoice.lean

Statistics

Metric	Count
Definitions axiom_unique_choice, unique_choice, unique_choice_fun	3
Theorems unique_choice_fun_spec, unique_choice_fun_unique, unique_choice_spec, unique_choice_unique, unique_subtype	5
Total	8

(root)

Definitions

Name	Category	Theorems
axiom_unique_choice 📖	MathAb	—
unique_choice 📖	CompOp	2 math math: unique_choice_spec, unique_choice_unique
unique_choice_fun 📖	CompOp	2 math math: unique_choice_fun_spec, unique_choice_fun_unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
unique_choice_fun_spec 📖	mathematical	—	unique_choice_fun	—	unique_choice_spec
unique_choice_fun_unique 📖	mathematical	—	unique_choice_fun	—	unique_choice_unique
unique_choice_spec 📖	mathematical	—	unique_choice	—	axiom_unique_choice unique_subtype
unique_choice_unique 📖	mathematical	—	unique_choice	—	unique_choice_spec
unique_subtype 📖	—	—	—	—	—

---

← Back to Index