isAtomic — Mathlib

English

For any x, the lower set {y ∈ α | y ≤ x} is atomic as a subposet.

Русский

Для любого x нижний интервал {y ∈ α | y ≤ x} является атомарным как частично упорядоченное множество.

LaTeX

$$$ IsAtomic (Set.Iic x).Elem $$$

Lean4

instance isAtomic {x : α} : IsAtomic (Set.Iic x) :=
  ⟨fun ⟨y, hy⟩ =>
    (eq_bot_or_exists_atom_le y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, hay.trans hy⟩, ha.Iic (hay.trans hy), hay⟩⟩

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