instMul — Mathlib

English

For any two upper sets S,T ⊆ α, their product S * T is the upper set { xy | x ∈ S, y ∈ T }. The carrier is the set of all products.

Русский

Для любых верхних множеств S и T над α их произведение S * T задаётся как {xy | x ∈ S, y ∈ T}. Облако остаётся верхним множеством.

LaTeX

$$$S,T \\in \\text{UpperSet}(\\alpha) \\implies S * T = \\{xy : x \\in S, y \\in T\\}$$$

Lean4

@[to_additive]
instance : Mul (UpperSet α) :=
  ⟨fun s t ↦ ⟨image2 (· * ·) s t, s.2.mul_right⟩⟩

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