English
A poset with a top element is coatomic if every nonempty chain not containing the top has an upper bound below the top.
Русский
Порядок с верхним элементом коатомный, если любая непустая цепь, не содержащая верхнего элемента, имеет верхнюю грань ниже верха.
LaTeX
$$$$\text{IsCoatomic } \alpha \iff \ \forall c, IsChain (\\le) c \to c.Nonempty \to ⊤ \notin c \to \exists x \neq ⊤, x \in upperBounds c.$$$$
Lean4
/-- **Zorn's lemma**: A partial order is coatomic if every nonempty chain `c`, `⊤ ∉ c`, has an upper
bound not equal to `⊤`. -/
theorem of_isChain_bounded {α : Type*} [PartialOrder α] [OrderTop α]
(h : ∀ c : Set α, IsChain (· ≤ ·) c → c.Nonempty → ⊤ ∉ c → ∃ x ≠ ⊤, x ∈ upperBounds c) : IsCoatomic α :=
by
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩
have := zorn_le_nonempty₀ (Ico x ⊤) (fun c hxc hc y hy => ?_) x (left_mem_Ico.2 hx)
· obtain ⟨y, hxy, hmax⟩ := this
refine ⟨y, ⟨hmax.prop.2.ne, fun z hyz ↦ le_top.eq_or_lt.resolve_right fun hz => ?_⟩, hxy⟩
exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le
rcases h c hc ⟨y, hy⟩ fun h => (hxc h).2.ne rfl with ⟨z, hz, hcz⟩
exact ⟨z, ⟨le_trans (hxc hy).1 (hcz hy), hz.lt_top⟩, hcz⟩
