mem_vars_bind₁ — Mathlib

English

Every variable occurring in bind₁ f φ comes from some variable i occurring in φ and from a variable appearing in f(i).

Русский

Любая переменная, встречающаяся в bind₁ f φ, берется из некоторой переменной i, встречающейся в φ, и из переменных, встречающихся в f(i).

LaTeX

$$$$ \forall j \in (\mathrm{bind}_1\, f\, \varphi).\mathrm{vars}, \; \exists i \in \mathrm{var}(\varphi),\; j \in (f(i)).\mathrm{vars} $$$$

Lean4

theorem mem_vars_bind₁ (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) {j : τ} (h : j ∈ (bind₁ f φ).vars) :
    ∃ i : σ, i ∈ φ.vars ∧ j ∈ (f i).vars := by
  classical simpa only [exists_prop, Finset.mem_biUnion, mem_support_iff, Ne] using vars_bind₁ f φ h

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