DependsOn

📁 Source: Mathlib/Logic/Function/DependsOn.lean

Statistics

Metric	Count
Definitions DependsOn	1
Theorems empty, mono, dependsOn_restrict, dependsOn_const, dependsOn_iff_exists_comp, dependsOn_iff_factorsThrough, dependsOn_univ	7
Total	8

DependsOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty 📖	—	DependsOn Set Set.instEmptyCollection	—	—	instIsEmptyFalse
mono 📖	—	Set Set.instHasSubset DependsOn	—	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_restrict 📖	mathematical	—	DependsOn restrict	—	—

(root)

Definitions

Name	Category	Theorems
DependsOn 📖	MathDef	13 math math: Preorder.dependsOn_restrictLe, dependsOn_univ, Set.dependsOn_restrict, Measurable.dependsOn_of_piFinset, MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset, Finset.dependsOn_restrict, MeasureTheory.dependsOn_cylinder_indicator_const, Preorder.dependsOn_frestrictLe, Measurable.dependsOn_of_piLE, dependsOn_const, MeasureTheory.StronglyMeasurable.dependsOn_of_piLE, dependsOn_iff_exists_comp, dependsOn_iff_factorsThrough

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_const 📖	mathematical	—	DependsOn Set Set.instEmptyCollection	—	instIsEmptyFalse
dependsOn_iff_exists_comp 📖	mathematical	—	DependsOn Set.restrict	—	dependsOn_iff_factorsThrough Function.factorsThrough_iff
dependsOn_iff_factorsThrough 📖	mathematical	—	DependsOn Function.FactorsThrough Set.restrict	—	DependsOn.eq_1 Function.FactorsThrough.eq_1
dependsOn_univ 📖	mathematical	—	DependsOn Set.univ	—	—

---

← Back to Index