isAtomic_iff_forall_isAtomic_Iic — Mathlib

English

An order with bottom is atomic if and only if every principal lower set (-∞, x] is atomic inside the interval.

Русский

Порядок с нижней границей атомарен тогда и только тогда, когда каждый интервал (-∞, x] атомарен внутри интервала.

LaTeX

$$$ IsAtomic α \iff \forall x:α, IsAtomic (Set.Iic x).Elem $$$

Lean4

theorem isAtomic_iff_forall_isAtomic_Iic [OrderBot α] : IsAtomic α ↔ ∀ x : α, IsAtomic (Set.Iic x) :=
  ⟨@IsAtomic.Set.Iic.isAtomic _ _ _, fun h =>
    ⟨fun x =>
      ((@eq_bot_or_exists_atom_le _ _ _ (h x)) (⊤ : Set.Iic x)).imp Subtype.mk_eq_mk.1
        (Exists.imp' (↑) fun ⟨_, _⟩ => And.imp_left IsAtom.of_isAtom_coe_Iic)⟩⟩

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