English
If e is an injective map from ι to κ, and if every c outside the range of e has g(c) ≥ 1, and f ≤ g ∘ e, then the HasProd bound for f is no larger than that for g.
Русский
Пусть e: ι → κ — инъекция, и для всякого c вне образа e выполняется g(c) ≥ 1, а также f(i) ≤ g(e(i)) для всех i. Тогда HasProd f a1 ≤ HasProd g a2.
LaTeX
$$$\\forall f,g, e:\\, ι \\to κ:\\, \\text{Injective } e \\to (\\forall c, c \\notin \\mathrm{range}(e) \\to 1 \\le g(c)) \\to (\\forall i, f(i) \\le g(e(i))) \\to \\text{HasProd } f\\, a_1 \\to \\text{HasProd } g\\, a_2 \\to a_1 \\le a_2$$$
Lean4
@[to_additive]
theorem hasProd_le_inj {g : κ → α} (e : ι → κ) (he : Injective e) (hs : ∀ c, c ∉ Set.range e → 1 ≤ g c)
(h : ∀ i, f i ≤ g (e i)) (hf : HasProd f a₁) (hg : HasProd g a₂) : a₁ ≤ a₂ :=
by
rw [← hasProd_extend_one he] at hf
refine hasProd_le (fun c ↦ ?_) hf hg
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
· rw [he.extend_apply]
exact h _
· rw [extend_apply' _ _ _ h]
exact hs _ h
