lowerClosure_mul — Mathlib

English

For all s,t ⊆ α, the lower closure distributes over multiplication: lowerClosure(s) · t = lowerClosure(s · t).

Русский

Нижнее замыкание распределяется по умножению: нижнее_замыкание(s) · t = нижнее_замыкание(s · t).

LaTeX

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

Lean4

@[to_additive]
theorem lowerClosure_mul : ↑(lowerClosure s) * t = lowerClosure (s * t) :=
  by
  simp_rw [mul_comm _ t]
  exact mul_lowerClosure _ _

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