coeffs_relation_subset_coeffs — Mathlib

English

Any coefficient that appears in a relation lies in the global coefficients set of the presentation.

Русский

Любой коэффициент из отношения принадлежит общему множеству коэффициентов презентации.

LaTeX

$$$((P.relation\\ x).coeffs : Set R) \\subseteq P.coeffs$$$

Lean4

theorem coeffs_relation_subset_coeffs (x : σ) : ((P.relation x).coeffs : Set R) ⊆ P.coeffs :=
  Set.subset_iUnion_of_subset x (by simp)

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