supIrredLowerSet — Mathlib

English

The Birkhoff embedding is the order-embedding sending a to the pair (Iic a, supIrred Iic a).

Русский

Встраивание Биркгоффа — это отображение-встраивание, отправляющее a в пару (Iic a, supIrred Iic a).

LaTeX

$$supIrredLowerSet : α ↪o { s : LowerSet α // SupIrred s }$$

Lean4

/-- The **Birkhoff Embedding** of a finite partial order as sup-irreducible elements in its
lattice of lower sets. -/
def supIrredLowerSet : α ↪o { s : LowerSet α // SupIrred s }
    where
  toFun a := ⟨Iic a, supIrred_Iic _⟩
  inj' _ := by simp
  map_rel_iff' := by simp

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