restrict_of_comp_subtype — Mathlib

English

If AlgebraicIndependent R (Function.comp x Subtype.val) holds on a subset s, then AlgebraicIndependent R (s.restrict x).

Русский

Если подмножество индексов s сохраняет алгебраическую независимость для x, то ограничение на s сохраняет независимость.

LaTeX

$$$\\text{AlgebraicIndependent}_R (\\mathrm{Function}.restrict x) $$$

Lean4

theorem restrict_of_comp_subtype {s : Set ι} (hs : AlgebraicIndependent R (x ∘ (↑) : s → A)) :
    AlgebraicIndependent R (s.restrict x) :=
  hs

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