isEmpty_algebraicIndependent — Mathlib

English

If the map algebraMap R A is not injective, then the set { s : Set A // AlgebraicIndepOn R id s } is empty.

Русский

Если отображение algebraMap R A не инъективно, то множество { s ⊆ A | AlgebraicIndepOn R id s } пусто.

LaTeX

$$$\\\\lnot\\\\ Injective(\\\\text{algebraMap } R A) \\\\Rightarrow \\\\text{IsEmpty}\\\\{s : Set A // AlgebraicIndepOn R id s\\\\}$$$

Lean4

theorem isEmpty_algebraicIndependent (h : ¬Injective (algebraMap R A)) :
    IsEmpty { s : Set A // AlgebraicIndepOn R id s } where false s := h s.2.algebraMap_injective

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