set_mul_subset — Mathlib

English

If s ⊆ I where I is a two-sided ideal, then t·s ⊆ I for any set t (i.e., multiplying s on the left by any t keeps the result in I).

Русский

Если s ⊆ I и I — двусторонний идеал, то для любого множества t верно t·s ⊆ I.

LaTeX

$$$s \\subseteq I \\Rightarrow t \\cdot s \\subseteq I$$$

Lean4

theorem set_mul_subset {s : Set R} {I : TwoSidedIdeal R} (h : s ⊆ I) (t : Set R) : t * s ⊆ I :=
  by
  rintro - ⟨r, -, x, hx, rfl⟩
  exact mul_mem_left _ _ _ (h hx)

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