infs_singleton — Mathlib

English

Let s be a finite set and b an element. The infimum with the singleton {b} distributes over s: s ⊼ {b} = { x ∧ b : x ∈ s }. Equivalently, intersect each element of s with b.

Русский

Пусть s — конечное множество и b — элемент. Инфинум с единичным множеством {b} распределяется по s: s ⊼ {b} = { x ∧ b : x ∈ s }. Иными словами, взять на каждом элементе s максимум по b.

LaTeX

$$$ s \⊼ \{b\} = \{ x \wedge b \; | \; x \in s \} $$$

Lean4

@[simp]
theorem infs_singleton : s ⊼ { b } = s.image (· ⊓ b) :=
  image₂_singleton_right

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