supported_strictMono — Mathlib

English

The map s ↦ supported(R,s) is strictly monotone: s ⊊ t implies supported(R,s) < supported(R,t).

Русский

Отображение s ↦ supported(R,s) строго монотонно: если s ⊊ t, то supported(R,s) < supported(R,t).

LaTeX

$$$$ s \\subsetneq t \\;\Rightarrow\; \\mathrm{supported}(R,s) < \\mathrm{supported}(R,t) $$$$

Lean4

theorem supported_strictMono [Nontrivial R] : StrictMono (supported R : Set σ → Subalgebra R (MvPolynomial σ R)) :=
  strictMono_of_le_iff_le fun _ _ ↦ supported_le_supported_iff.symm

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