English
The variables appearing in bind₁ f φ are contained in the union of the variables appearing in φ and the variables appearing in the images f(i).
Русский
Переменные, участвующие в bind₁ f φ, лежат в объединении переменных φ и переменных образов f(i).
LaTeX
$$$$ (\mathrm{bind}_1\, f\, \varphi).\mathrm{vars} \subseteq \varphi.{\mathrm vars} \cup \bigcup_{i \in \varphi.\mathrm vars} (f i).\mathrm vars $$$$
Lean4
theorem vars_bind₁ [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
(bind₁ f φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars :=
by
calc
(bind₁ f φ).vars
_ = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars := by rw [← map_sum, ← φ.as_sum]
_ ≤ φ.support.biUnion fun i : σ →₀ ℕ => ((bind₁ f) (monomial i (coeff i φ))).vars := (vars_sum_subset _ _)
_ = φ.support.biUnion fun d : σ →₀ ℕ => vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) := by
simp only [bind₁_monomial]
_ ≤ φ.support.biUnion fun d : σ →₀ ℕ => d.support.biUnion fun i => vars (f i) :=
?_
-- proof below
_ ≤ φ.vars.biUnion fun i : σ => vars (f i) :=
?_
-- proof below
· apply Finset.biUnion_mono
intro d _hd
calc
vars (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i) ≤ (C (coeff d φ)).vars ∪ (∏ i ∈ d.support, f i ^ d i).vars :=
vars_mul _ _
_ ≤ (∏ i ∈ d.support, f i ^ d i).vars := by
simp only [Finset.empty_union, vars_C, Finset.le_iff_subset, Finset.Subset.refl]
_ ≤ d.support.biUnion fun i : σ => vars (f i ^ d i) := (vars_prod _)
_ ≤ d.support.biUnion fun i : σ => (f i).vars := ?_
apply Finset.biUnion_mono
intro i _hi
apply vars_pow
· intro j
simp_rw [Finset.mem_biUnion]
rintro ⟨d, hd, ⟨i, hi, hj⟩⟩
exact ⟨i, (mem_vars _).mpr ⟨d, hd, hi⟩, hj⟩
