birkhoffSet_inf — Mathlib

English

The image of a greatest lower bound under the Birkhoff embedding is the intersection of the images of the summands.

Русский

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

LaTeX

$$$\\operatorname{birkhoffSet}(a \\wedge b) = \\operatorname{birkhoffSet}(a) \\cap \\operatorname{birkhoffSet}(b)$$$

Lean4

@[simp]
theorem birkhoffSet_inf (a b : α) : birkhoffSet (a ⊓ b) = birkhoffSet a ∩ birkhoffSet b := by
  unfold OrderEmbedding.birkhoffSet; split <;> simp [eq_iff_true_of_subsingleton]

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