mono — Mathlib

English

If t ⊆ s and the elements indexed by s are algebraically independent, then the elements indexed by t are algebraically independent.

Русский

Если t ⊆ s и элементы, индексируемые через s, алгебраически независимы, то и элементы через t независимы.

LaTeX

$$$t\\subseteq s \\Rightarrow \\text{AlgebraicIndependent } R\\, (\\mathrm{Subtype}.val \\mid_s) \\Rightarrow \\text{AlgebraicIndependent } R\\, (\\mathrm{Subtype}.val \\mid_t)$$$

Lean4

theorem mono {t s : Set A} (h : t ⊆ s) (hx : AlgebraicIndependent R ((↑) : s → A)) :
    AlgebraicIndependent R ((↑) : t → A) := by simpa [Function.comp] using hx.comp (inclusion h) (inclusion_injective h)

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