min_le_mk_mul — Mathlib

English

The minimum of the Archimedean classes mk a and mk b is not greater than mk(a b).

Русский

Минимум классов mk a и mk b не превосходит mk(a b).

LaTeX

$$\min (mk a) (mk b) \le mk (a b)$$

Lean4

@[to_additive]
theorem min_le_mk_mul (a b : M) : min (mk a) (mk b) ≤ mk (a * b) :=
  by
  by_contra! h
  rw [lt_min_iff] at h
  have h1 := (mk_lt_mk.mp h.1 2).trans_le (mabs_mul_le _ _)
  have h2 := (mk_lt_mk.mp h.2 2).trans_le (mabs_mul_le _ _)
  simp only [mul_lt_mul_iff_left, mul_lt_mul_iff_right, pow_two] at h1 h2
  exact h1.not_gt h2

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