完備

sup__inf.v

Section SupInf.
Variable S : Type.
Variable R : S -> S -> Prop.
Infix ">=" := R.
Infix "<=" := (fun x y => y >= x).
Definition subset : Type := S -> Prop.
Definition element (X : subset) (x : S) : Prop := X x.
Definition upper_bound (X : subset) (u : S) : Prop :=
  forall x, element X x -> u >= x.
Definition lower_bound (X : subset) (u : S) : Prop :=
  forall x, element X x -> u <= x.
Definition supremum (X : subset) (s : S) : Prop :=
  (upper_bound X s) /¥ (forall u, upper_bound X u -> u >= s).
Definition infimum (X : subset) (s : S) : Prop :=
  (lower_bound X s) /¥ (forall u, lower_bound X u -> u <= s).
Definition not_empty (X : subset) := exists x, element X x.
Variable upper_bound__sup : forall X, not_empty X
  -> (exists u, upper_bound X u) -> (exists s, supremum X s).
Theorem  lower_bound__inf : forall X, not_empty X
  -> (exists u, lower_bound X u) -> (exists s, infimum X s).
Proof.
intros X [x Hnempty] [u Hlb].
pose (L := (fun u => lower_bound X u) : subset). simpl in L.
assert (Hsup : exists s, supremum L s).
  apply upper_bound__sup.
  exists u. assumption.
  exists x. intros u' HLu'. unfold element, L in HLu'. apply HLu'. assumption.
destruct Hsup as [s [Hub Hmin]].
exists s. split.
- intros x' HXx'. apply Hmin. intros u' HLu'. unfold element, L in HLu'.
  apply HLu'. assumption.
- intros l' Hlbl'. apply Hub. unfold element, L. assumption.
Qed.
End SupInf.