isSimpleOrder_Iic_iff_isAtom — Mathlib

English

For any a, the lower interval Iic(a) is simple if and only if a is an atom.

Русский

Для любого a монадный отрезок Iic(a) прост, если и только если a является атомом.

LaTeX

$$$\text{IsSimpleOrder}(\mathrm{Iic}(a)) \iff \text{IsAtom}(a)$$$

Lean4

theorem isSimpleOrder_Iic_iff_isAtom [PartialOrder α] [OrderBot α] {a : α} : IsSimpleOrder (Iic a) ↔ IsAtom a :=
  isSimpleOrder_iff_isAtom_top.trans <|
    and_congr (not_congr Subtype.mk_eq_mk)
      ⟨fun h b ab => Subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab), fun h ⟨b, _⟩ hbotb =>
        Subtype.mk_eq_mk.2 (h b (Subtype.mk_lt_mk.1 hbotb))⟩

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