infIrredUpperSet — Mathlib

English

The Birkhoff embedding into inf-irreducible upper sets maps a to (Ici a, infIrred ICI a).

Русский

Встраивание Биркгоффа в InfIrred верхних множеств отправляет a в (Ici a, infIrred ICI a).

LaTeX

$$infIrredUpperSet : α ↪o { s : UpperSet α // InfIrred s }$$

Lean4

/-- The **Birkhoff Embedding** of a finite partial order as inf-irreducible elements in its
lattice of lower sets. -/
def infIrredUpperSet : α ↪o { s : UpperSet α // InfIrred s }
    where
  toFun a := ⟨Ici a, infIrred_Ici _⟩
  inj' _ := by simp
  map_rel_iff' := by simp

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