feat(order/zorn): upward inclusion variant of Zorn's lemma (#7362)

add zorn_superset

This also add various missing bits of whitespace throughout the file.

src/order/zorn.lean

@@ -22,25 +22,27 @@ local infix ` ≺ `:50  := r
 
 /-- A chain is a subset `c` satisfying
   `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ c`. -/
-def chain (c : set α) := pairwise_on c (λx y, x ≺ y ∨ y ≺ x)
+def chain (c : set α) := pairwise_on c (λ x y, x ≺ y ∨ y ≺ x)
 parameters {r}
 
 theorem chain.total_of_refl [is_refl α r]
   {c} (H : chain c) {x y} (hx : x ∈ c) (hy : y ∈ c) :
   x ≺ y ∨ y ≺ x :=
 if e : x = y then or.inl (e ▸ refl _) else H _ hx _ hy e
 
-theorem chain.mono {c c'} : c' ⊆ c → chain c → chain c' :=
+theorem chain.mono {c c'} :
+  c' ⊆ c → chain c → chain c' :=
 pairwise_on.mono
 
-theorem chain.directed_on [is_refl α r] {c} (H : chain c) : directed_on (≺) c :=
+theorem chain.directed_on [is_refl α r] {c} (H : chain c) :
+  directed_on (≺) c :=
 assume x hx y hy,
 match H.total_of_refl hx hy with
 | or.inl h := ⟨y, hy, h, refl _⟩
 | or.inr h := ⟨x, hx, refl _, h⟩
 end
 
-theorem chain_insert {c : set α} {a : α} (hc : chain c) (ha : ∀b∈c, b ≠ a → a ≺ b ∨ b ≺ a) :
+theorem chain_insert {c : set α} {a : α} (hc : chain c) (ha : ∀ b ∈ c, b ≠ a → a ≺ b ∨ b ≺ a) :
   chain (insert a c) :=
 forall_insert_of_forall
   (assume x hx, forall_insert_of_forall (hc x hx) (assume hneq, (ha x hx hneq).symm))
@@ -51,22 +53,23 @@ forall_insert_of_forall
 def super_chain (c₁ c₂ : set α) : Prop := chain c₂ ∧ c₁ ⊂ c₂
 
 /-- A chain `c` is a maximal chain if there does not exists a chain strictly including `c`. -/
-def is_max_chain (c : set α) := chain c ∧ ¬ (∃c', super_chain c c')
+def is_max_chain (c : set α) := chain c ∧ ¬ (∃ c', super_chain c c')
 
 /-- Given a set `c`, if there exists a chain `c'` strictly including `c`, then `succ_chain c`
 is one of these chains. Otherwise it is `c`. -/
 def succ_chain (c : set α) : set α :=
-if h : ∃c', chain c ∧ super_chain c c' then some h else c
+if h : ∃ c', chain c ∧ super_chain c c' then some h else c
 
-theorem succ_spec {c : set α} (h : ∃c', chain c ∧ super_chain c c') :
+theorem succ_spec {c : set α} (h : ∃ c', chain c ∧ super_chain c c') :
   super_chain c (succ_chain c) :=
 let ⟨c', hc'⟩ := h in
 have chain c ∧ super_chain c (some h),
   from @some_spec _ (λc', chain c ∧ super_chain c c') _,
 by simp [succ_chain, dif_pos, h, this.right]
 
-theorem chain_succ {c : set α} (hc : chain c) : chain (succ_chain c) :=
-if h : ∃c', chain c ∧ super_chain c c' then
+theorem chain_succ {c : set α} (hc : chain c) :
+  chain (succ_chain c) :=
+if h : ∃ c', chain c ∧ super_chain c c' then
   (succ_spec h).left
 else
   by simp [succ_chain, dif_neg, h]; exact hc
@@ -79,29 +82,32 @@ begin
   exact succ_spec ⟨c', hc₁, hc'⟩
 end
 
-theorem succ_increasing {c : set α} : c ⊆ succ_chain c :=
-if h : ∃c', chain c ∧ super_chain c c' then
+theorem succ_increasing {c : set α} :
+  c ⊆ succ_chain c :=
+if h : ∃ c', chain c ∧ super_chain c c' then
   have super_chain c (succ_chain c), from succ_spec h,
   this.right.left
 else by simp [succ_chain, dif_neg, h, subset.refl]
 
 /-- Set of sets reachable from `∅` using `succ_chain` and `⋃₀`. -/
 inductive chain_closure : set α → Prop
-| succ : ∀{s}, chain_closure s → chain_closure (succ_chain s)
-| union : ∀{s}, (∀a∈s, chain_closure a) → chain_closure (⋃₀ s)
+| succ : ∀ {s}, chain_closure s → chain_closure (succ_chain s)
+| union : ∀ {s}, (∀ a ∈ s, chain_closure a) → chain_closure (⋃₀ s)
 
-theorem chain_closure_empty : chain_closure ∅ :=
+theorem chain_closure_empty :
+  chain_closure ∅ :=
 have chain_closure (⋃₀ ∅),
   from chain_closure.union $ assume a h, h.rec _,
 by simp at this; assumption
 
-theorem chain_closure_closure : chain_closure (⋃₀ chain_closure) :=
+theorem chain_closure_closure :
+  chain_closure (⋃₀ chain_closure) :=
 chain_closure.union $ assume s hs, hs
 
 variables {c c₁ c₂ c₃ : set α}
 
 private lemma chain_closure_succ_total_aux (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
-  (h : ∀{c₃}, chain_closure c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain c₃ ⊆ c₂) :
+  (h : ∀ {c₃}, chain_closure c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ succ_chain c₃ ⊆ c₂) :
   c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁ :=
 begin
   induction hc₁,
@@ -147,13 +153,15 @@ begin
     { exact (h₁ $ subset.trans succ_increasing h) } }
 end
 
-theorem chain_closure_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
+theorem chain_closure_total (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂) :
+  c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
 have c₁ ⊆ c₂ ∨ succ_chain c₂ ⊆ c₁,
   from chain_closure_succ_total_aux hc₁ hc₂ $ assume c₃ hc₃, chain_closure_succ_total hc₃ hc₂,
 or.imp_right (assume : succ_chain c₂ ⊆ c₁, subset.trans succ_increasing this) this
 
 theorem chain_closure_succ_fixpoint (hc₁ : chain_closure c₁) (hc₂ : chain_closure c₂)
-  (h_eq : succ_chain c₂ = c₂) : c₁ ⊆ c₂ :=
+  (h_eq : succ_chain c₂ = c₂) :
+  c₁ ⊆ c₂ :=
 begin
   induction hc₁,
   case succ : c₁ hc₁ h {
@@ -175,13 +183,14 @@ theorem chain_closure_succ_fixpoint_iff (hc : chain_closure c) :
       ... = c : this.symm)
     succ_increasing⟩
 
-theorem chain_chain_closure (hc : chain_closure c) : chain c :=
+theorem chain_chain_closure (hc : chain_closure c) :
+  chain c :=
 begin
   induction hc,
   case succ : c hc h {
     exact chain_succ h },
   case union : s hs h {
-    have h : ∀c∈s, zorn.chain c := h,
+    have h : ∀ c ∈ s, zorn.chain c := h,
     exact assume c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq,
       have t₁ ⊆ t₂ ∨ t₂ ⊆ t₁, from chain_closure_total (hs _ ht₁) (hs _ ht₂),
       or.elim this
@@ -196,7 +205,8 @@ def max_chain := ⋃₀ chain_closure
 
 There exists a maximal totally ordered subset of `α`.
 Note that we do not require `α` to be partially ordered by `r`. -/
-theorem max_chain_spec : is_max_chain max_chain :=
+theorem max_chain_spec :
+  is_max_chain max_chain :=
 classical.by_contradiction $
 assume : ¬ is_max_chain (⋃₀ chain_closure),
 have super_chain (⋃₀ chain_closure) (succ_chain (⋃₀ chain_closure)),
@@ -210,12 +220,12 @@ h₃ this.symm
 /-- Zorn's lemma
 
 If every chain has an upper bound, then there is a maximal element -/
-theorem exists_maximal_of_chains_bounded
-  (h : ∀c, chain c → ∃ub, ∀a∈c, a ≺ ub) (trans : ∀{a b c}, a ≺ b → b ≺ c → a ≺ c) :
-  ∃m, ∀a, m ≺ a → a ≺ m :=
-have ∃ub, ∀a∈max_chain, a ≺ ub,
+theorem exists_maximal_of_chains_bounded (h : ∀ c, chain c → ∃ ub, ∀ a ∈ c, a ≺ ub)
+  (trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) :
+  ∃ m, ∀ a, m ≺ a → a ≺ m :=
+have ∃ ub, ∀ a ∈ max_chain, a ≺ ub,
   from h _ $ max_chain_spec.left,
-let ⟨ub, (hub : ∀a∈max_chain, a ≺ ub)⟩ := this in
+let ⟨ub, (hub : ∀ a ∈ max_chain, a ≺ ub)⟩ := this in
 ⟨ub, assume a ha,
   have chain (insert a max_chain),
     from chain_insert max_chain_spec.left $ assume b hb _, or.inr $ trans (hub b hb) ha,
@@ -229,8 +239,9 @@ If every nonempty chain of a nonempty type has an upper bound, then there is a m
 (A variant of Zorn's lemma.)
 -/
 theorem exists_maximal_of_nonempty_chains_bounded [nonempty α]
-  (h : ∀c, chain c → c.nonempty → ∃ub, ∀a∈c, a ≺ ub) (trans : ∀{a b c}, a ≺ b → b ≺ c → a ≺ c) :
-  ∃m, ∀a, m ≺ a → a ≺ m :=
+  (h : ∀ c, chain c → c.nonempty → ∃ ub, ∀ a ∈ c, a ≺ ub)
+  (trans : ∀ {a b c}, a ≺ b → b ≺ c → a ≺ c) :
+  ∃ m, ∀ a, m ≺ a → a ≺ m :=
 exists_maximal_of_chains_bounded
   (λ c hc,
     (eq_empty_or_nonempty c).elim
@@ -240,13 +251,20 @@ exists_maximal_of_chains_bounded
 
 end chain
 
+--This lemma isn't under section `chain` because `parameters` messes up with it. Feel free to fix it
+/-- This can be used to turn `zorn.chain (≥)` into `zorn.chain (≤)` and vice-versa. -/
+theorem chain.symm {α : Type u} {s : set α} {q : α → α → Prop} (h : chain q s) :
+  chain (flip q) s :=
+h.mono' (λ _ _, or.symm)
+
 theorem zorn_partial_order {α : Type u} [partial_order α]
-  (h : ∀c:set α, chain (≤) c → ∃ub, ∀a∈c, a ≤ ub) : ∃m:α, ∀a, m ≤ a → a = m :=
+  (h : ∀ c : set α, chain (≤) c → ∃ ub, ∀ a ∈ c, a ≤ ub) :
+  ∃ m : α, ∀ a, m ≤ a → a = m :=
 let ⟨m, hm⟩ := @exists_maximal_of_chains_bounded α (≤) h (assume a b c, le_trans) in
 ⟨m, assume a ha, le_antisymm (hm a ha) ha⟩
 
 theorem zorn_nonempty_partial_order {α : Type u} [partial_order α] [nonempty α]
-  (h : ∀ (c : set α), chain (≤) c → c.nonempty → ∃ub, ∀ a ∈ c, a ≤ ub) :
+  (h : ∀ (c : set α), chain (≤) c → c.nonempty → ∃ ub, ∀ a ∈ c, a ≤ ub) :
   ∃ (m : α), ∀ a, m ≤ a → a = m :=
 let ⟨m, hm⟩ := @exists_maximal_of_nonempty_chains_bounded α (≤) _ h (λ a b c, le_trans) in
 ⟨m, λ a ha, le_antisymm (hm a ha) ha⟩
@@ -263,8 +281,8 @@ let ⟨⟨m, hms⟩, h⟩ := @zorn_partial_order {m // m ∈ s} _
 in ⟨m, hms, λ z hzs hmz, congr_arg subtype.val (h ⟨z, hzs⟩ hmz)⟩
 
 theorem zorn_nonempty_partial_order₀ {α : Type u} [partial_order α] (s : set α)
-  (ih : ∀ c ⊆ s, chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub)
-  (x : α) (hxs : x ∈ s) : ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m :=
+  (ih : ∀ c ⊆ s, chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α) (hxs : x ∈ s) :
+  ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m :=
 let ⟨⟨m, hms, hxm⟩, h⟩ := @zorn_partial_order {m // m ∈ s ∧ x ≤ m} _
   (λ c hc, c.eq_empty_or_nonempty.elim
     (assume hce, hce.symm ▸ ⟨⟨x, hxs, le_refl _⟩, λ _, false.elim⟩)
@@ -277,24 +295,33 @@ let ⟨⟨m, hms, hxm⟩, h⟩ := @zorn_partial_order {m // m ∈ s ∧ x ≤ m}
 ⟨m, hms, hxm, λ z hzs hmz, congr_arg subtype.val $ h ⟨z, hzs, le_trans hxm hmz⟩ hmz⟩
 
 theorem zorn_subset {α : Type u} (S : set (set α))
-  (h : ∀c ⊆ S, chain (⊆) c → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
-  ∃ m ∈ S, ∀a ∈ S, m ⊆ a → a = m :=
+  (h : ∀ c ⊆ S, chain (⊆) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
+  ∃ m ∈ S, ∀ a ∈ S, m ⊆ a → a = m :=
 zorn_partial_order₀ S h
 
 theorem zorn_subset_nonempty {α : Type u} (S : set (set α))
-  (H : ∀c ⊆ S, chain (⊆) c → c.nonempty → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) (x) (hx : x ∈ S) :
-  ∃ m ∈ S, x ⊆ m ∧ ∀a ∈ S, m ⊆ a → a = m :=
+  (H : ∀ c ⊆ S, chain (⊆) c → c.nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) (x) (hx : x ∈ S) :
+  ∃ m ∈ S, x ⊆ m ∧ ∀ a ∈ S, m ⊆ a → a = m :=
 zorn_nonempty_partial_order₀ _ (λ c cS hc y yc, H _ cS hc ⟨y, yc⟩) _ hx
 
-theorem chain.total {α : Type u} [preorder α]
-  {c : set α} (H : chain (≤) c) :
+theorem zorn_superset {α : Type u} (S : set (set α))
+  (h : ∀ c ⊆ S, chain (⊆) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) :
+  ∃ m ∈ S, ∀ a ∈ S, a ⊆ m → a = m :=
+@zorn_partial_order₀ (order_dual (set α)) _ S $ λ c cS hc, h c cS hc.symm
+
+theorem zorn_superset_nonempty {α : Type u} (S : set (set α))
+  (H : ∀ c ⊆ S, chain (⊆) c → c.nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) (x) (hx : x ∈ S) :
+  ∃ m ∈ S, m ⊆ x ∧ ∀ a ∈ S, a ⊆ m → a = m :=
+@zorn_nonempty_partial_order₀ (order_dual (set α)) _ S (λ c cS hc y yc, H _ cS
+  hc.symm ⟨y, yc⟩) _ hx
+
+theorem chain.total {α : Type u} [preorder α] {c : set α} (H : chain (≤) c) :
   ∀ {x y}, x ∈ c → y ∈ c → x ≤ y ∨ y ≤ x :=
 λ x y, H.total_of_refl
 
-theorem chain.image {α β : Type*} (r : α → α → Prop)
-  (s : β → β → Prop) (f : α → β)
-  (h : ∀ x y, r x y → s (f x) (f y))
-  {c : set α} (hrc : chain r c) : chain s (f '' c) :=
+theorem chain.image {α β : Type*} (r : α → α → Prop) (s : β → β → Prop) (f : α → β)
+  (h : ∀ x y, r x y → s (f x) (f y)) {c : set α} (hrc : chain r c) :
+  chain s (f '' c) :=
 λ x ⟨a, ha₁, ha₂⟩ y ⟨b, hb₁, hb₂⟩, ha₂ ▸ hb₂ ▸ λ hxy,
   (hrc a ha₁ b hb₁ (mt (congr_arg f) $ hxy)).elim
     (or.inl ∘ h _ _) (or.inr ∘ h _ _)
@@ -303,7 +330,7 @@ end zorn
 
 theorem directed_of_chain {α β r} [is_refl β r] {f : α → β} {c : set α}
   (h : zorn.chain (f ⁻¹'o r) c) :
-  directed r (λx:{a:α // a ∈ c}, f x) :=
+  directed r (λ x : {a : α // a ∈ c}, f x) :=
 assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases
   (assume : a = b, by simp only [this, exists_prop, and_self, subtype.exists];
     exact ⟨b, hb, refl _⟩)