birkhoffFinset_sup — Mathlib

English

The finset version of the Birkhoff embedding preserves suprema via union.

Русский

Финитный набор сохраняет супремумы через объединение.

LaTeX

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

Lean4

@[simp]
theorem birkhoffFinset_sup (a b : α) : birkhoffFinset (a ⊔ b) = birkhoffFinset a ∪ birkhoffFinset b := by
  classical
  dsimp [OrderEmbedding.birkhoffFinset]
  rw [birkhoffSet_sup, OrderIso.coe_toOrderEmbedding]
  simp

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