ChainCompleteness.lean

1import Mathlib.Order.Zorn2import Mathlib.Order.Bounds.Basic34/-! # Detecting incompleteness by a chain -/56namespace BFPP78set_option autoImplicit false9open Set1011variable {B : Type*} [SemilatticeSup B]1213/-- Chain completeness implies completeness in a join semilattice.14The empty chain is included in the hypothesis. -/15theorem exists_isLUB_of_chain_complete16    (hchain : ∀ c : Set B, IsChain (· ≤ ·) c → ∃ b, IsLUB c b) (s : Set B) :17    ∃ b, IsLUB s b := by18  let L := lowerBounds (upperBounds s)19  obtain ⟨m, hm⟩ := zorn_le₀ L (by20    intro c hc hcc21    obtain ⟨b, hb⟩ := hchain c hcc22    refine ⟨b, ?_, fun z hz => hb.1 hz⟩23    intro u hu24    exact hb.2 (fun z hz => hc hz hu))25  refine ⟨m, ?_, hm.prop⟩26  intro x hx27  have hxL : x ∈ L := fun u hu => hu hx28  have hsup : m ⊔ x ∈ L := fun u hu => sup_le (hm.prop hu) (hxL hu)29  exact le_sup_right.trans (hm.2 hsup le_sup_left)3031theorem exists_chain_without_isLUB (h : ∃ s : Set B, ¬ ∃ b, IsLUB s b) :32    ∃ c : Set B, IsChain (· ≤ ·) c ∧ ¬ ∃ b, IsLUB c b := by33  classical34  by_contra hn35  have hall : ∀ c : Set B, IsChain (· ≤ ·) c → ∃ b, IsLUB c b := by36    intro c hc37    by_contra hb38    exact hn ⟨c, hc, hb⟩39  obtain ⟨s, hs⟩ := h40  exact hs (exists_isLUB_of_chain_complete hall s)4142end BFPP

SHA-256