dependsOn_univ — Mathlib

English

For any f, f depends on the universal set (i.e., all coordinates).

Русский

Для любой функции f зависимость распространяется на все координаты (полная независимость от входных переменных).

LaTeX

$$$DependsOn\!f\,univ \iff \forall x,y:\; (\forall i, x(i)=y(i)) \rightarrow f(x)=f(y)$$$

Lean4

theorem dependsOn_univ (f : (Π i, α i) → β) : DependsOn f univ := fun _ _ h ↦ congrArg _ <| funext fun i ↦ h i trivial

Похожие утверждения