birkhoffSet_sup — Mathlib

English

The image of a least upper bound under the Birkhoff embedding is the union of the images of the summands.

Русский

Изображение наименьшего верхнего предела через вложение Биркхоффа равно объединению изображений составляющих.

LaTeX

$$$\\operatorname{birkhoffSet}(a \\vee b) = \\operatorname{birkhoffSet}(a) \\cup \\operatorname{birkhoffSet}(b)$$$

Lean4

@[simp]
theorem birkhoffSet_sup (a b : α) : birkhoffSet (a ⊔ b) = birkhoffSet a ∪ birkhoffSet b := by
  unfold OrderEmbedding.birkhoffSet; split <;> simp [eq_iff_true_of_subsingleton]

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