mul_subset_closure — Mathlib

English

For subsets S, T of a monoid M, the closure of S · T is below the supremum of closures: closure(S T) ≤ closure(S) ⊔ closure(T).

Русский

Замыкание множества S T относительно операции умножения меньше или равно верхней границе закрытий S и T.

LaTeX

$$$ closure (S * T) \leq closure S \; \sqcup\; closure T $$$

Lean4

@[to_additive]
theorem mul_subset_closure (hs : s ⊆ u) (ht : t ⊆ u) : s * t ⊆ Submonoid.closure u :=
  mul_subset (Subset.trans hs Submonoid.subset_closure) (Subset.trans ht Submonoid.subset_closure)

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