singleton_infs — Mathlib

English

Let t be a finite set and a a fixed element. The infimum with the singleton {a} distributes over t by taking pairwise infima: {a} ⊼ t = { a ∧ x : x ∈ t }. In words, intersecting each element of t with a yields the infimum-constructed set.

Русский

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

LaTeX

$$$ {a} \vDash t = \{ a \wedge x \; | \; x \in t \} $$$

Lean4

@[simp]
theorem singleton_infs : { a } ⊼ t = t.image (a ⊓ ·) :=
  image₂_singleton_left

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