lowerClosure_mul_distrib — Mathlib

English

Lower closure distributes over multiplication: lowerClosure(s · t) = lowerClosure(s) · lowerClosure(t).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem lowerClosure_mul_distrib : lowerClosure (s * t) = lowerClosure s * lowerClosure t :=
  SetLike.coe_injective <| by rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]

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