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