English
If each α_i has a compatible order, multiplication, and the ExistsMulOfLE property, then the product ∏_{i} α_i has ExistsMulOfLE. In other words, for any a,b in the product with a ≤ b coordinatewise, there exists c in the product such that a_i c_i ≤ b_i for all i, obtained coordinatewise from the witness in each component.
Русский
Если для каждого i имеется упорядочение и умножение, и для каждого α_i выполнено свойство ExistsMulOfLE, то произведение ∏_{i} α_i также имеет это свойство: для любых a,b в произведении с a_i ≤ b_i по каждому i существует c в произведении, такой что a_i c_i ≤ b_i для всех i (по координатам).
LaTeX
$$$\\forall a,b : \\prod_{i\\in I} \\alpha_i,\\ (\\forall i, a_i \\le b_i) \\Rightarrow \\exists c : \\prod_{i\\in I} \\alpha_i,\\ \\forall i, a_i c_i \\le b_i.$$$
Lean4
@[to_additive]
instance existsMulOfLe {ι : Type*} {α : ι → Type*} [∀ i, LE (α i)] [∀ i, Mul (α i)] [∀ i, ExistsMulOfLE (α i)] :
ExistsMulOfLE (∀ i, α i) :=
⟨fun h => ⟨fun i => (exists_mul_of_le <| h i).choose, funext fun i => (exists_mul_of_le <| h i).choose_spec⟩⟩
