src/HOL/Real/HahnBanach/Bounds.thy
author wenzelm
Sat Dec 16 21:41:51 2000 +0100 (2000-12-16)
changeset 10687 c186279eecea
parent 9503 3324cbbecef8
child 13515 a6a7025fd7e8
permissions -rw-r--r--
tuned HOL/Real/HahnBanach;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Bounds.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@9035
     6
header {* Bounds *}
wenzelm@7808
     7
wenzelm@9035
     8
theory Bounds = Main + Real:
wenzelm@7535
     9
wenzelm@10687
    10
text {*
wenzelm@10687
    11
  A supremum\footnote{The definition of the supremum is based on one
wenzelm@10687
    12
  in \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}
wenzelm@10687
    13
  of an ordered set @{text B} w.~r.~t. @{text A} is defined as a least
wenzelm@10687
    14
  upper bound of @{text B}, which lies in @{text A}.
wenzelm@10687
    15
*}
wenzelm@7535
    16
   
wenzelm@10687
    17
text {*
wenzelm@10687
    18
  If a supremum exists, then @{text "Sup A B"} is equal to the
wenzelm@10687
    19
  supremum. *}
wenzelm@7535
    20
wenzelm@7535
    21
constdefs
wenzelm@10687
    22
  is_Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool"
wenzelm@10687
    23
  "is_Sup A B x \<equiv> isLub A B x"
wenzelm@7535
    24
wenzelm@10687
    25
  Sup :: "('a::order) set \<Rightarrow> 'a set \<Rightarrow> 'a"
wenzelm@10687
    26
  "Sup A B \<equiv> Eps (is_Sup A B)"
wenzelm@7917
    27
wenzelm@10687
    28
text {*
wenzelm@10687
    29
  The supremum of @{text B} is less than any upper bound of
wenzelm@10687
    30
  @{text B}. *}
wenzelm@7535
    31
wenzelm@10687
    32
lemma sup_le_ub: "isUb A B y \<Longrightarrow> is_Sup A B s \<Longrightarrow> s \<le> y"
wenzelm@9035
    33
  by (unfold is_Sup_def, rule isLub_le_isUb)
wenzelm@7535
    34
wenzelm@10687
    35
text {* The supremum @{text B} is an upper bound for @{text B}. *}
wenzelm@7917
    36
wenzelm@10687
    37
lemma sup_ub: "y \<in> B \<Longrightarrow> is_Sup A B s \<Longrightarrow> y \<le> s"
wenzelm@9035
    38
  by (unfold is_Sup_def, rule isLubD2)
wenzelm@7535
    39
wenzelm@10687
    40
text {*
wenzelm@10687
    41
  The supremum of a non-empty set @{text B} is greater than a lower
wenzelm@10687
    42
  bound of @{text B}. *}
wenzelm@7917
    43
wenzelm@7917
    44
lemma sup_ub1: 
wenzelm@10687
    45
  "\<forall>y \<in> B. a \<le> y \<Longrightarrow> is_Sup A B s \<Longrightarrow> x \<in> B \<Longrightarrow> a \<le> s"
wenzelm@9035
    46
proof - 
wenzelm@10687
    47
  assume "\<forall>y \<in> B. a \<le> y"  "is_Sup A B s"  "x \<in> B"
wenzelm@10687
    48
  have "a \<le> x" by (rule bspec)
wenzelm@10687
    49
  also have "x \<le> s" by (rule sup_ub)
wenzelm@10687
    50
  finally show "a \<le> s" .
wenzelm@9035
    51
qed
wenzelm@7535
    52
  
wenzelm@10687
    53
end