upperClosure_mul — Mathlib

English

For all s,t ⊆ α, the upper closure of s, multiplied by t, equals the upper closure of s·t: upperClosure(s) · t = upperClosure(s · t).

Русский

Для любых подмножеств s,t ⊆ α верно: верхнее_замыкание(s) · t = верхнее_замыкание(s · t).

LaTeX

$$$\forall s,t \subseteq \alpha:\; \operatorname{upperClosure}(s) \cdot t = \operatorname{upperClosure}(s \cdot t)$$$

Lean4

@[to_additive]
theorem upperClosure_mul : ↑(upperClosure s) * t = upperClosure (s * t) :=
  by
  simp_rw [mul_comm _ t]
  exact mul_upperClosure _ _

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