mul_lowerClosure — Mathlib

English

For all sets s,t ⊆ α, the product of s with the lower closure of t equals the lower closure of the product: s · lowerClosure(t) = lowerClosure(s · t).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_lowerClosure : s * lowerClosure t = lowerClosure (s * t) :=
  by
  simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul, LowerSet.coe_iSup₂]
  rfl

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