sSup_mul_distrib — Mathlib

English

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

Русский

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

LaTeX

$$$\\\\forall x \\\\in \\\\alpha,\n\\\\forall s \\\\subseteq \\\\alpha, \\\\operatorname{sSup}(s) \\\\cdot x = \\\\bigvee_{y \\\\in s} (y \\\\cdot x).$$$

Lean4

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

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