upperClosure_mul_distrib — Mathlib

English

Upper closure distributes over multiplication: upperClosure(s · t) = upperClosure(s) · upperClosure(t).

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem upperClosure_mul_distrib : upperClosure (s * t) = upperClosure s * upperClosure t :=
  SetLike.coe_injective <| by rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]

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