mem_vars_rename — Mathlib

English

If j is in the renamed polynomial’s variables, then there exists i with i in φ.vars and f i = j.

Русский

Если j ∈ rename f φ. vars, существует i ∈ φ.vars и f i = j.

LaTeX

$$$ \exists i, i \in φ.vars \land f i = j $$$

Lean4

theorem mem_vars_rename (f : σ → τ) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ (rename f φ).vars) :
    ∃ i : σ, i ∈ φ.vars ∧ f i = j := by classical simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

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