mul_left_mem_add_closure — Mathlib

English

The product of an element a ∈ S and an element b ∈ closure(S) lies in closure(S).

Русский

Произведение элемента a ∈ S и элемента b ∈ closure(S) принадлежит closure(S).

LaTeX

$$$a \in S \land b \in \overline{S} \Rightarrow ab \in \overline{S}$$$

Lean4

/-- The product of an element of `S` and an element of the additive closure of a multiplicative
submonoid `S` is contained in the additive closure of `S`. -/
theorem mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ closure (S : Set R)) : a * b ∈ closure (S : Set R) :=
  mul_mem_add_closure (mem_closure.mpr fun _sT hT => hT ha) hb

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