coe_birkhoffFinset — Mathlib

English

The finset-based encoding of the Birkhoff representation coincides with the set-based encoding at the level of elements.

Русский

Кодирование представления Биркхоффа через конечный набор совпадает с кодированием через множества на уровне элементов.

LaTeX

$$$\\text{birkhoffFinset}(a) = \\text{birkhoffSet}(a)$$$

Lean4

@[simp]
theorem coe_birkhoffFinset (a : α) : birkhoffFinset a = birkhoffSet a := by
  classical
    -- TODO: This should be a single `simp` call but `simp` refuses to use
      -- `OrderIso.coe_toOrderEmbedding` and `Fintype.coe_finsetOrderIsoSet_symm`
    simp [birkhoffFinset, (OrderIso.coe_toOrderEmbedding)]

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