Iic_eq — Mathlib

English

Let a be an atom in a poset with a least element. Then the downward set of a, Iic(a), consists exactly of the bottom element and a itself.

Русский

Пусть a — атом в частично упорядоченном множестве с нулём. Тогда множество элементов, не превосходящих a, состоит ровно из ⊥ и a.

LaTeX

$$$ \\mathrm{Iic}(a) = \\{ \\bot, a \\}$$$

Lean4

theorem Iic_eq (h : IsAtom a) : Set.Iic a = {⊥, a} :=
  Set.ext fun _ => h.le_iff

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