coeffs_relation_mem_range — Mathlib

English

For any x ∈ σ, the coefficients of the relation P.relation x lie in the base coefficient range from R0 to R.

Русский

Для любого x ∈ σ коэффициенты отношения P.relation x лежат в базовом диапазоне коэффициентов от R0 к R.

LaTeX

$$$\\forall x,\\ ↑(P.relation x).coeffs \\subseteq \\mathrm{Set.range}(\\mathrm{algebraMap}\\,R_0\\,R)$$$

Lean4

theorem coeffs_relation_mem_range (x : σ) : ↑(P.relation x).coeffs ⊆ Set.range (algebraMap R₀ R) :=
  subset_trans (P.coeffs_relation_subset_coeffs x) HasCoeffs.coeffs_subset_range

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