Quelle Linearform.thy Sprache: Isabelle

(*  Title:      HOL/Hahn_Banach/Linearform.thy
    Author:     Gertrud Bauer, TU Munich
*)

section \<open>Linearforms\<close>

theory Linearform
imports Vector_Space
begin

text \<open>
  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
  additive and multiplicative.
\<close>

locale linearform =
  fixes V :: "'a::{minus, plus, zero, uminus} set" and f
  assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y"
    and mult [iff]: "x \ V \ f (a \ x) = a * f x"

declare linearform.intro [intro?]

lemma (in linearform) neg [iff]:
  assumes "vectorspace V"
  shows "x \ V \ f (- x) = - f x"
proof -
  interpret vectorspace V by fact
  assume x: "x \ V"
  then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)
  also from x have "\ = (- 1) * (f x)" by (rule mult)
  also from x have "\ = - (f x)" by simp
  finally show ?thesis .
qed

lemma (in linearform) diff [iff]:
  assumes "vectorspace V"
  shows "x \ V \ y \ V \ f (x - y) = f x - f y"
proof -
  interpret vectorspace V by fact
  assume x: "x \ V" and y: "y \ V"
  then have "x - y = x + - y" by (rule diff_eq1)
  also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y)
  also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg)
  finally show ?thesis by simp
qed

text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>

lemma (in linearform) zero [iff]:
  assumes "vectorspace V"
  shows "f 0 = 0"
proof -
  interpret vectorspace V by fact
  have "f 0 = f (0 - 0)" by simp
  also have "\ = f 0 - f 0" using \vectorspace V\ by (rule diff) simp_all
  also have "\ = 0" by simp
  finally show ?thesis .
qed

end

quality98%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.