Theorems · Definition
DependsOn
{ι : Type u_1} → {α : ι → Type u_2} → {β : Type u_3} → (((i : ι) → α i) → β) → Set ι → PropA function f depends on s if, whenever x and y coincide over s, f x = f y.
It should be interpreted as "f _potentially_ depends only on variables in s".
However it might be the case that f does not depend at all on variables in s,
for example if f is constant. As a consequence, DependsOn f univ is always true,
see dependsOn_univ.
- Defined in
- Mathlib.Logic.Function.DependsOn
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
Cited by23
Results whose statement or proof uses this declaration.
- dependsOn_iff_factorsThroughstatement · cited by 5
- Set.dependsOn_domRestrictstatement · cited by 3
- DependsOn.dependsOn_lmarginalPartialTrajstatement and proof · cited by 2
- DependsOn.lmarginalPartialTraj_of_lestatement and proof · cited by 2
- DependsOn.updateFinsetstatement and proof · cited by 2
- MeasureTheory.dependsOn_cylinder_indicator_conststatement · cited by 1
- MeasureTheory.StronglyMeasurable.dependsOn_of_piFinsetstatement · cited by 1
- MeasureTheory.StronglyMeasurable.dependsOn_of_piLEstatement · cited by 1
- DependsOn.lmarginalPartialTraj_const_rightstatement and proof · cited by 1
- Finset.dependsOn_restrictstatement · cited by 1
- ProbabilityTheory.Kernel.le_lmarginalPartialTraj_succstatement and proof · cited by 1
- ProbabilityTheory.Kernel.trajContent_tendsto_zeroproof · cited by 1