dependsOn_iff_factorsThrough — Mathlib

English

For any f and any s, f depends on s if and only if f factors through the restriction to s; i.e., there exists a function on (Π i : s, α i) whose composition with the restriction to s equals f.

Русский

Для любой функции f и любого множества s: f зависит от s тогда и только тогда, когда f факторизуется через ограничение на s; то есть существует функция g на (Π i : s, α i), такая что f = g ∘ restrict.

LaTeX

$$$DependsOn(f,s) \iff FactorsThrough(f, s.restrict)$$$

Lean4

theorem dependsOn_iff_factorsThrough {f : (Π i, α i) → β} {s : Set ι} : DependsOn f s ↔ FactorsThrough f s.restrict :=
  by
  rw [DependsOn, FactorsThrough]
  simp [funext_iff]

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