mul_sSup_distrib — Mathlib

English

Let α be a semigroup with CompleteLattice structure and IsQuantale. Then for any x and a set s, x · sSup s = ⨆ y ∈ s, x · y.

Русский

Пусть α — полугруппа с полным локальным замыканием и IsQuantale. Тогда для любого x и множества s выполняется x · sSup s = ⨆ y ∈ s, x · y.

LaTeX

$$$\\\\forall x \\\\in \\\\alpha, \\\\forall s \\\\subseteq \\\\alpha, x \\\\cdot \\operatorname{sSup}(s) = \\\\operatorname{S-u-p} (\\\\{ y \\\\in s \\\\mid y \\\\in s \\\\}) \\\\text{(}`x·sSup(s)=⨆ y ∈ s, x·y)`.$$

Lean4

@[to_additive]
theorem mul_sSup_distrib : x * sSup s = ⨆ y ∈ s, x * y :=
  IsQuantale.mul_sSup_distrib _ _

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