hasInfs — Mathlib

English

The pairwise infimum operation on Finsets, s ⊼ t, consists of all elements a ⊓ b with a ∈ s and b ∈ t.

Русский

Операция попарного инфимума над Finset: s ⊼ t = { a ⊓ b | a ∈ s, b ∈ t }.

LaTeX

$$$ s ⊼ t = \{ a \sqcap b \mid a \in s, b \in t \} $$$

Lean4

/-- `s ⊼ t` is the finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`. -/
protected def hasInfs : HasInfs (Finset α) :=
  ⟨image₂ (· ⊓ ·)⟩

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