Theory Consumers

(* License: LGPL *)
(*
Author: Julian Parsert <julian.parsert@gmail.com>
Author: Cezary Kaliszyk
*)


section ‹ Consumers  ›

text ‹ Consumption sets ›


theory Consumers
  imports                 
    "HOL-Analysis.Multivariate_Analysis"
    "../Syntax"
begin

subsection ‹ Pre Arrow-Debreu consumption set ›

text ‹ It turns out that the First Welfare Theorem does
       not require any particular limitations on the consumption set ›
locale pre_arrow_debreu_consumption_set =
  fixes consumption_set :: "('a::euclidean_space) set"
  assumes "x ∈ (UNIV:: 'a set) ⟹ x ∈ consumption_set"
begin
end


subsection ‹ Arrow-Debreu model consumption set›

text ‹ The Arrow-Debreu model consumption set includes more and stricter
        assumptions which are necessary for further results. ›
locale gen_pre_arrow_debreu_consum_set =
  fixes consumption_set :: "('a::ordered_euclidean_space) set"
begin

end

locale arrow_debreu_consum_set =
  fixes consumption_set :: "('a::ordered_euclidean_space) set"
  assumes r_plus: "consumption_set ⊆ {(x::'a). x ≥ 0}"
  assumes closed: "closed consumption_set"
  assumes convex: "convex consumption_set"
  assumes non_empty: "consumption_set ≠ {}"
  assumes "∀M ∈ consumption_set. (∀x > M. x ∈ consumption_set)" (*unbounded above*)
begin

lemma x_larger_0: "x ∈ consumption_set ⟹ x ≥ 0"
  using r_plus by auto

lemma larger_in_consump_set:
  "x ∈ consumption_set ∧ y ≥ x ⟹ y ∈ consumption_set"
  using arrow_debreu_consum_set_axioms arrow_debreu_consum_set_def
    dual_order.order_iff_strict by fastforce

end

end