English
For two polynomials p1 and p2 in MvPolynomial σ R there exist a finite set s ⊆ σ and polynomials q1, q2 in MvPolynomial s R such that p1 = rename (↑) q1 and p2 = rename (↑) q2.
Русский
Для двух полиномов p1 и p2 в MvPolynomial σ R существует конечное множество s ⊆ σ и полиномы q1, q2 в MvPolynomial s R такие, что p1 = rename (↑) q1 и p2 = rename (↑) q2.
LaTeX
$$$ \exists s\;\exists q_1\;\exists q_2\;\; p_1 = rename (↑) q_1 \land p_2 = rename (↑) q_2 $$$
Lean4
/-- `exists_finset_rename` for two polynomials at once: for any two polynomials `p₁`, `p₂` in a
polynomial semiring `R[σ]` of possibly infinitely many variables, `exists_finset_rename₂` yields
a finite subset `s` of `σ` such that both `p₁` and `p₂` are contained in the polynomial semiring
`R[s]` of finitely many variables. -/
theorem exists_finset_rename₂ (p₁ p₂ : MvPolynomial σ R) :
∃ (s : Finset σ) (q₁ q₂ : MvPolynomial s R), p₁ = rename (↑) q₁ ∧ p₂ = rename (↑) q₂ :=
by
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
classical
use s₁ ∪ s₂
use rename (Set.inclusion s₁.subset_union_left) q₁
use rename (Set.inclusion s₁.subset_union_right) q₂
constructor <;> simp [Function.comp_def]
