supported_eq_range_rename — Mathlib

English

The subalgebra of polynomials supported by s equals the range of rename Subtype.val; i.e., supported R s = (rename (Subtype.val)).range.

Русский

Подалгебра полиномов, поддерживаемых множеством s, равна образу rename Subtype.val; т.е. supported R s = (rename (Subtype.val)).range.

LaTeX

$$$ \text{supported } R s = (\mathrm{rename} (\uparrow)).\mathrm{range} $$$

Lean4

theorem supported_eq_range_rename (s : Set σ) : supported R s = (rename ((↑) : s → σ)).range :=
  by
  rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]
  congr

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