hasInfs — Mathlib

English

There is a binary operation on sets, s ⊼ t, defined by taking all infima a ⊓ b with a ∈ s and b ∈ t.

Русский

Существует бинарная операция над множествами, s ⊼ t, заданная как множество инфимумов a ⊓ b, где a ∈ s, b ∈ t.

LaTeX

$$$ \\text{HasInfs}(\\text{Set }\\alpha) \\;:\\; s ⊼ t := \\{ a \\sqcap 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 hasInfs : HasInfs (Set α) :=
  ⟨image2 (· ⊓ ·)⟩

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