mem_supported — Mathlib

English

A polynomial p is in the support subalgebra on s if and only if all its variables lie in s; formally p ∈ supported R s iff p.vars ⊆ s.

Русский

Полином p лежит в подалгебре, поддерживаемой s, тогда и только тогда, когда все переменные p лежат в s: p ∈ supported R s ⇔ p.vars ⊆ s.

LaTeX

$$$ p \in \text{supported } R s \; \Leftrightarrow \uparrow p.vars \subseteq s $$$

Lean4

theorem mem_supported : p ∈ supported R s ↔ ↑p.vars ⊆ s := by
  classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

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