feat(set_theory/ordinal): add conditionally_complete_linear_order_bot…

… instance (#9266)

Currently, it is not possible to talk about `Inf s` when `s` is a set of ordinals. This is fixed by this PR.

src/order/conditionally_complete_lattice.lean

@@ -118,6 +118,57 @@ instance conditionally_complete_linear_order_of_complete_linear_order [complete_
   conditionally_complete_linear_order α :=
 { ..conditionally_complete_lattice_of_complete_lattice, .. ‹complete_linear_order α› }
 
+section
+open_locale classical
+
+/-- A well founded linear order is conditionally complete, with a bottom element. -/
+@[reducible] noncomputable def well_founded.conditionally_complete_linear_order_with_bot
+  {α : Type*} [i : linear_order α] (h : well_founded ((<) : α → α → Prop))
+  (c : α) (hc : c = h.min set.univ ⟨c, mem_univ c⟩) :
+  conditionally_complete_linear_order_bot α :=
+{ sup := max,
+  le_sup_left := le_max_left,
+  le_sup_right := le_max_right,
+  sup_le := λ a b c, max_le,
+  inf := min,
+  inf_le_left := min_le_left,
+  inf_le_right := min_le_right,
+  le_inf := λ a b c, le_min,
+  Inf := λ s, if hs : s.nonempty then h.min s hs else c,
+  cInf_le := begin
+    assume s a hs has,
+    have s_ne : s.nonempty := ⟨a, has⟩,
+    simpa [s_ne] using not_lt.1 (h.not_lt_min s s_ne has),
+  end,
+  le_cInf := begin
+    assume s a hs has,
+    simp only [hs, dif_pos],
+    exact has (h.min_mem s hs),
+  end,
+  Sup := λ s, if hs : (upper_bounds s).nonempty then h.min _ hs else c,
+  le_cSup := begin
+    assume s a hs has,
+    have h's : (upper_bounds s).nonempty := hs,
+    simp only [h's, dif_pos],
+    exact h.min_mem _ h's has,
+  end,
+  cSup_le := begin
+    assume s a hs has,
+    have h's : (upper_bounds s).nonempty := ⟨a, has⟩,
+    simp only [h's, dif_pos],
+    simpa using h.not_lt_min _ h's has,
+  end,
+  bot := c,
+  bot_le := λ x, by convert not_lt.1 (h.not_lt_min set.univ ⟨c, mem_univ c⟩ (mem_univ x)),
+  cSup_empty := begin
+    have : (set.univ : set α).nonempty := ⟨c, mem_univ c⟩,
+    simp only [this, dif_pos, upper_bounds_empty],
+    exact hc.symm
+  end,
+  .. i }
+
+end
+
 section order_dual
 
 instance (α : Type*) [conditionally_complete_lattice α] :
@@ -238,6 +289,12 @@ lemma cInf_upper_bounds_eq_cSup {s : set α} (h : bdd_above s) (hs : s.nonempty)
   Inf (upper_bounds s) = Sup s :=
 (is_glb_cInf h $ hs.mono $ λ x hx y hy, hy hx).unique (is_lub_cSup hs h).is_glb
 
+lemma not_mem_of_lt_cInf {x : α} {s : set α} (h : x < Inf s) (hs : bdd_below s) : x ∉ s :=
+λ hx, lt_irrefl _ (h.trans_le (cInf_le hs hx))
+
+lemma not_mem_of_cSup_lt {x : α} {s : set α} (h : Sup s < x) (hs : bdd_above s) : x ∉ s :=
+@not_mem_of_lt_cInf (order_dual α) _ x s h hs
+
 /--Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
 is larger than all elements of `s`, and that this is not the case of any `w<b`.
 See `Sup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/

src/set_theory/ordinal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 -/
 import set_theory.cardinal
+import order.conditionally_complete_lattice
 
 /-!
 # Ordinals
@@ -49,6 +50,10 @@ initial segment (or, equivalently, in any way). This total order is well founded
 * `cardinal.ord c`: when `c` is a cardinal, `ord c` is the smallest ordinal with this cardinality.
   It is the canonical way to represent a cardinal with an ordinal.
 
+A conditionally complete linear order with bot structure is registered on ordinals, where `⊥` is
+`0`, the ordinal corresponding to the empty type, and `Inf` is `ordinal.omin` for nonempty sets
+and `0` for the empty set by convention.
+
 ## Notations
 * `r ≼i s`: the type of initial segment embeddings of `r` into `s`.
 * `r ≺i s`: the type of principal segment embeddings of `r` into `s`.
@@ -696,6 +701,12 @@ end⟩⟩
 
 instance : has_well_founded ordinal := ⟨(<), wf⟩
 
+/-- Reformulation of well founded induction on ordinals as a lemma that works with the
+`induction` tactic, as in `induction i using ordinal.induction with i IH`. -/
+lemma induction {p : ordinal.{u} → Prop} (i : ordinal.{u})
+  (h : ∀ j, (∀ k, k < j → p k) → p j) : p i :=
+ordinal.wf.induction i h
+
 /-- Principal segment version of the `typein` function, embedding a well order into
   ordinals as a principal segment. -/
 def typein.principal_seg {α : Type u} (r : α → α → Prop) [is_well_order α r] :
@@ -1102,6 +1113,28 @@ let ⟨i, e⟩ := min_eq I (lift ∘ f) in
 by rw e; exact lift_le.2 (le_min.2 $ λ j, lift_le.1 $
 by have := min_le (lift ∘ f) j; rwa e at this)
 
+instance : conditionally_complete_linear_order_bot ordinal :=
+wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (ordinal.zero_le _) $
+  not_lt.1 (wf.not_lt_min set.univ ⟨0, mem_univ _⟩ (mem_univ 0))
+
+@[simp] lemma bot_eq_zero : (⊥ : ordinal) = 0 := rfl
+
+lemma Inf_eq_omin {s : set ordinal} (hs : s.nonempty) :
+  Inf s = omin s hs :=
+begin
+  simp only [Inf, conditionally_complete_lattice.Inf, omin, conditionally_complete_linear_order.Inf,
+    conditionally_complete_linear_order_bot.Inf, hs, dif_pos],
+  congr,
+  rw subtype.range_val,
+end
+
+lemma Inf_mem {s : set ordinal} (hs : s.nonempty) :
+  Inf s ∈ s :=
+by { rw Inf_eq_omin hs, exact omin_mem _ hs }
+
+instance : no_top_order ordinal :=
+⟨λ a, ⟨a.succ, lt_succ_self a⟩⟩
+
 end ordinal
 
 /-! ### Representing a cardinal with an ordinal -/