dependsOn_restrict — Mathlib

English

The restricted family over s depends only on the underlying set of s, not on any particular presentation of s as a Finset; formally, the restriction map is determined by s as a subset.

Русский

Ограничение семейства над s зависит только от множества, лежащего в основе s, а не от конкретного представления s как Finset.

LaTeX

$$$\\text{DependsOn}(s.\\restriction(\\pi),\u00A0s).$$$

Lean4

theorem dependsOn_restrict (s : Finset ι) : DependsOn (s.restrict (π := π)) s :=
  (s : Set ι).dependsOn_restrict

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