Ioi_mul_Ici_subset' — Mathlib

English

For all a,b, the product Ioi(a)·Ici(b) is contained in Ioi(ab): Ioi(a)·Ici(b) ⊆ Ioi(ab).

Русский

Для любых a,b произведение Ioi(a) и Ici(b) содержится в Ioi(ab).

LaTeX

$$$$ Ioi(a) \\cdot Ici(b) \\subseteq Ioi(a b). $$$$

Lean4

@[to_additive Ioi_add_Ici_subset]
theorem Ioi_mul_Ici_subset' (a b : α) : Ioi a * Ici b ⊆ Ioi (a * b) :=
  by
  have := mulLeftMono_of_mulLeftStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_lt_of_le hya hzb

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