Up to index of Isabelle/HOL/HOL-Complex/HahnBanach
theory Bounds(* Title: HOL/Real/HahnBanach/Bounds.thy ID: $Id: Bounds.thy,v 1.16 2005/06/17 14:13:09 haftmann Exp $ Author: Gertrud Bauer, TU Munich *) header {* Bounds *} theory Bounds imports Main Real begin locale lub = fixes A and x assumes least [intro?]: "(!!a. a ∈ A ==> a ≤ b) ==> x ≤ b" and upper [intro?]: "a ∈ A ==> a ≤ x" lemmas [elim?] = lub.least lub.upper constdefs the_lub :: "'a::order set => 'a" "the_lub A ≡ The (lub A)" syntax (xsymbols) the_lub :: "'a::order set => 'a" ("\<Squnion>_" [90] 90) lemma the_lub_equality [elim?]: includes lub shows "\<Squnion>A = (x::'a::order)" proof (unfold the_lub_def) from lub_axioms show "The (lub A) = x" proof fix x' assume lub': "lub A x'" show "x' = x" proof (rule order_antisym) from lub' show "x' ≤ x" proof fix a assume "a ∈ A" then show "a ≤ x" .. qed show "x ≤ x'" proof fix a assume "a ∈ A" with lub' show "a ≤ x'" .. qed qed qed qed lemma the_lubI_ex: assumes ex: "∃x. lub A x" shows "lub A (\<Squnion>A)" proof - from ex obtain x where x: "lub A x" .. also from x have [symmetric]: "\<Squnion>A = x" .. finally show ?thesis . qed lemma lub_compat: "lub A x = isLub UNIV A x" proof - have "isUb UNIV A = (λx. A *<= x ∧ x ∈ UNIV)" by (rule ext) (simp only: isUb_def) then show ?thesis by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast qed lemma real_complete: fixes A :: "real set" assumes nonempty: "∃a. a ∈ A" and ex_upper: "∃y. ∀a ∈ A. a ≤ y" shows "∃x. lub A x" proof - from ex_upper have "∃y. isUb UNIV A y" by (unfold isUb_def setle_def) blast with nonempty have "∃x. isLub UNIV A x" by (rule reals_complete) then show ?thesis by (simp only: lub_compat) qed end
lemmas
[| lub A x; !!a. a ∈ A ==> a ≤ b |] ==> x ≤ b
[| lub A x; a ∈ A |] ==> a ≤ x
lemmas
[| lub A x; !!a. a ∈ A ==> a ≤ b |] ==> x ≤ b
[| lub A x; a ∈ A |] ==> a ≤ x
lemma the_lub_equality:
lub A x ==> the_lub A = x
lemma the_lubI_ex:
∃x. lub A x ==> lub A (the_lub A)
lemma lub_compat:
lub A x = isLub UNIV A x
lemma real_complete:
[| ∃a. a ∈ A; ∃y. ∀a∈A. a ≤ y |] ==> ∃x. lub A x