dependsOn_iff_exists_comp — Mathlib

English

For any s, there exists a function g on (Π i : s, α i) such that f = g ∘ s.restrict if and only if f depends on s.

Русский

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

LaTeX

$$$DependsOn(f,s) \iff \exists g: (Π i : s, α i) → β, \; f = g \circ s.restrict$$$

Lean4

theorem dependsOn_iff_exists_comp [Nonempty β] {f : (Π i, α i) → β} {s : Set ι} :
    DependsOn f s ↔ ∃ g : (Π i : s, α i) → β, f = g ∘ s.restrict := by
  rw [dependsOn_iff_factorsThrough, factorsThrough_iff]

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