English
The Birkhoff embedding of a finite poset maps each a to the pair (Iic a, supIrred Iic a) in the lattice of lower sets.
Русский
Встраивание Биркгоффа конечного частично упорядоченного множества отправляет элемент a в пару (Iic a, supIrred Iic a) в решетке нижних множеств.
LaTeX
$$$\text{supIrredLowerSet}(a) = \langle Iic(a), \text{supIrred\_Iic}(a) \rangle$$$
Lean4
@[simp]
theorem infIrred_Ici (a : α) : InfIrred (Ici a) :=
by
refine ⟨fun h ↦ Ici_ne_top h.eq_top, fun s t hst ↦ ?_⟩
have := mem_Ici_iff.2 (le_refl a)
rw [← hst] at this
exact
this.imp (fun ha ↦ le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_left) fun ha ↦
le_antisymm (le_Ici.2 ha) <| hst.ge.trans inf_le_right
