Basic results on conditionally complete partial orders

This file contains some basic results on conditionally complete partial orders, and is intended to parallel the API for conditionally complete lattices where possible. For the reason, the theorems here are mostly protected within the DirectedOn namespace, unless such an assumption is unnecessary. Otherwise the names here share the same names as their counterparts in Mathlib/Order/ConditionallyCompleteLattice/Basic.lean.

instance OrderDual.instConditionallyCompletePartialOrderInfOfConditionallyCompletePartialOrderSup {α : Type u_1} [ConditionallyCompletePartialOrderSup α] : ConditionallyCompletePartialOrderInf αᵒᵈ

instance OrderDual.instConditionallyCompletePartialOrderSupOfConditionallyCompletePartialOrderInf {α : Type u_1} [ConditionallyCompletePartialOrderInf α] : ConditionallyCompletePartialOrderSup αᵒᵈ

instance OrderDual.instConditionallyCompletePartialOrder {α : Type u_1} [ConditionallyCompletePartialOrder α] : ConditionallyCompletePartialOrder αᵒᵈ

theorem DirectedOn.le_csSup_of_le {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a b : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s

theorem DirectedOn.csInf_le_of_le {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a

theorem DirectedOn.csSup_le_csSup {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s t : Set α} (hds : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hdt : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) t) (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) : sSup s ≤ sSup t

theorem DirectedOn.csInf_le_csInf {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s t : Set α} (hds : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (hdt : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) t) (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s

theorem DirectedOn.le_csSup_iff {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (h : BddAbove s) (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

theorem DirectedOn.csInf_le_iff {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a

theorem IsGreatest.directedOn {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (H : IsGreatest s a) : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s

theorem IsLeast.directedOn {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (H : IsLeast s a) : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s

theorem IsGreatest.csSup_eq {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (H : IsGreatest s a) : sSup s = a

A greatest element of a set is the supremum of this set.

theorem IsLeast.csInf_eq {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (H : IsLeast s a) : sInf s = a

A least element of a set is the infimum of this set.

theorem IsGreatest.csSup_mem {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (H : IsGreatest s a) : sSup s ∈ s

theorem IsLeast.csInf_mem {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (H : IsLeast s a) : sInf s ∈ s

theorem DirectedOn.csSup_le_iff {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hb : BddAbove s) (hs : s.Nonempty) : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

theorem DirectedOn.le_csInf_iff {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

theorem DirectedOn.notMem_of_csSup_lt {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {x : α} {s : Set α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (h : sSup s < x) (hs : BddAbove s) : x ∉ s

theorem DirectedOn.notMem_of_lt_csInf {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {x : α} {s : Set α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (h : x < sInf s) (hs : BddBelow s) : x ∉ s

theorem DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {b : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b) (H' : ∀ w < b, ∃ a ∈ s, w < a) : sSup s = b

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 sSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in complete lattices.

theorem DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {b : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (hs : s.Nonempty) (H : ∀ a ∈ s, b ≤ a) (H' : ∀ (w : α), b < w → ∃ a ∈ s, a < w) : sInf s = b

Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w>b. See sInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in complete lattices.

theorem DirectedOn.lt_csSup_of_lt {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} {a b : α} (hd : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s

b < sSup s when there is an element a in s with b < a, when s is bounded above. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness above for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

theorem DirectedOn.csInf_lt_of_lt {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} {a b : α} (hd : DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) s) (hs : BddBelow s) (ha : a ∈ s) (h : a < b) : sInf s < b

sInf s < b when there is an element a in s with a < b, when s is bounded below. This is essentially an iff, except that the assumptions for the two implications are slightly different (one needs boundedness below for one direction, nonemptiness and linear order for the other one), so we formulate separately the two implications, contrary to the CompleteLattice case.

@[simp]

theorem csSup_singleton {α : Type u_1} [ConditionallyCompletePartialOrderSup α] (a : α) : sSup {a} = a

The supremum of a singleton is the element of the singleton

@[simp]

theorem csInf_singleton {α : Type u_1} [ConditionallyCompletePartialOrderInf α] (a : α) : sInf {a} = a

@[simp]

theorem csInf_Ici {α : Type u_5} [ConditionallyCompletePartialOrderInf α] {a : α} : sInf (Set.Ici a) = a

@[simp]

theorem csInf_Ico {α : Type u_5} [ConditionallyCompletePartialOrderInf α] {a b : α} (h : a < b) : sInf (Set.Ico a b) = a

@[simp]

theorem csInf_Icc {α : Type u_5} [ConditionallyCompletePartialOrderInf α] {a b : α} (h : a ≤ b) : sInf (Set.Icc a b) = a

@[simp]

theorem csSup_Iic {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {a : α} : sSup (Set.Iic a) = a

@[simp]

theorem csSup_Ioc {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {a b : α} (h : a < b) : sSup (Set.Ioc a b) = b

@[simp]

theorem csSup_Icc {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {a b : α} (h : a ≤ b) : sSup (Set.Icc a b) = b

theorem sup_eq_top_of_top_mem {α : Type u_1} [ConditionallyCompletePartialOrderSup α] {s : Set α} [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤

theorem inf_eq_bot_of_bot_mem {α : Type u_1} [ConditionallyCompletePartialOrderInf α] {s : Set α} [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥

theorem DirectedOn.subset_Icc_csInf_csSup {α : Type u_1} [ConditionallyCompletePartialOrder α] {s : Set α} (hdb : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s) (hda : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Set.Icc (sInf s) (sSup s)

theorem DirectedOn.csInf_le_csSup {α : Type u_1} [ConditionallyCompletePartialOrder α] {s : Set α} (hdb : DirectedOn (fun (x1 x2 : α) => x1 ≥ x2) s) (hda : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s) (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) : sInf s ≤ sSup s

If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.