Ici_mul_Ioi_subset' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive Ici_add_Ioi_subset]
theorem Ici_mul_Ioi_subset' (a b : α) : Ici a * Ioi b ⊆ Ioi (a * b) :=
  by
  have := mulRightMono_of_mulRightStrictMono α
  rintro x ⟨y, hya, z, hzb, rfl⟩
  exact mul_lt_mul_of_le_of_lt hya hzb

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