prod_mono — Mathlib

English

If a ≤ b in FactorSet, then a.prod ≤ b.prod (alternate formulation).

Русский

Если a ≤ b в FactorSet, то a.prod ≤ b.prod (альтернативная формулировка).

LaTeX

$$$a \le b \Rightarrow a.prod \le b.prod$$$

Lean4

@[gcongr]
theorem prod_mono : ∀ {a b : FactorSet α}, a ≤ b → a.prod ≤ b.prod
  | ⊤, b, h => by
    have : b = ⊤ := top_unique h
    rw [this, prod_top]
  | a, ⊤, _ => show a.prod ≤ (⊤ : FactorSet α).prod by simp
  | WithTop.some _, WithTop.some _, h => prod_le_prod <| Multiset.map_le_map <| WithTop.coe_le_coe.1 <| h

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