isSimpleOrder_Ici_iff_isCoatom — Mathlib

English

For any a, the upper interval Ici(a) is simple if and only if a is a coatom.

Русский

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

LaTeX

$$$\text{IsSimpleOrder}(\mathrm{Ici}(a)) \iff \text{IsCoatom}(a)$$$

Lean4

theorem isSimpleOrder_Ici_iff_isCoatom [PartialOrder α] [OrderTop α] {a : α} : IsSimpleOrder (Ici a) ↔ IsCoatom a :=
  isSimpleOrder_iff_isCoatom_bot.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))⟩

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