hasSups — Mathlib

English

The operation s ⊻ t on subsets is defined by taking all pairwise joins: s ⊻ t = { a ⊔ b | a ∈ s, b ∈ t }.

Русский

Операция s ⊻ t на подмножествaх задаётся как множество попарных объединений: s ⊻ t = { a ⊔ b | a ∈ s, b ∈ t }.

LaTeX

$$$ s \ ⊻ \ t := \{ a \ ⊔ \ b \mid a \in s,\; b \in t \}$$$

Lean4

/-- `s ⊻ t` is the set of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`. -/
protected def hasSups : HasSups (Set α) :=
  ⟨image2 (· ⊔ ·)⟩

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