birkhoffFinset_inf — Mathlib

English

The finset version of the Birkhoff embedding preserves infima via intersection.

Русский

Финитное отображение Биркхоффа сохраняет инфимы через пересечение.

LaTeX

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

Lean4

@[simp]
theorem birkhoffFinset_inf (a b : α) : birkhoffFinset (a ⊓ b) = birkhoffFinset a ∩ birkhoffFinset b := by
  classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_inf, OrderIso.coe_toOrderEmbedding]
  simp

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