mul_upperClosure — Mathlib

English

For any sets s,t ⊆ α, the product of s with the upper closure of t equals the upper closure of the product: s · upperClosure(t) = upperClosure(s · t).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_upperClosure : s * upperClosure t = upperClosure (s * t) :=
  by
  simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul, UpperSet.coe_iInf₂]
  rfl

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