Quelle Fun_More.thy Sprache: Isabelle

(*  Title:      HOL/Cardinals/Fun_More.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

More on injections, bijections and inverses.
*)

section \<open>More on Injections, Bijections and Inverses\<close>

theory Fun_More
  imports Main
begin

subsection \<open>Purely functional properties\<close>

(* unused *)
(*1*)lemma bij_betw_diff_singl:
  assumes BIJ: "bij_betw f A A'" and IN: "a \ A"
  shows "bij_betw f (A - {a}) (A' - {f a})"
proof-
  let ?B = "A - {a}"   let ?B' = "A' - {f a}"
  have "f a \ A'" using IN BIJ unfolding bij_betw_def by blast
  hence "a \ ?B \ f a \ ?B' \ A = ?B \ {a} \ A' = ?B' \ {f a}"
    using IN by blast
  thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp
qed

subsection \<open>Properties involving finite and infinite sets\<close>

(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT:
  assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'"
  shows "f `((inv_into A f)`B') = B'"
  by (metis BIJ SUB bij_betw_imp_surj_on image_inv_into_cancel)

(* unused *)
(*1*)lemma bij_betw_inv_into_RIGHT_LEFT:
  assumes BIJ: "bij_betw f A A'" and SUB: "B' \ A'" and
    IM: "(inv_into A f) ` B' = B"
  shows "f ` B = B'"
  by (metis BIJ IM SUB bij_betw_inv_into_RIGHT)

(* unused *)
(*2*)lemma bij_betw_inv_into_twice:
  assumes "bij_betw f A A'"
  shows "\a \ A. inv_into A' (inv_into A f) a = f a"
  by (simp add: assms inv_into_inv_into_eq)

subsection \<open>Properties involving Hilbert choice\<close>

(*1*)lemma bij_betw_inv_into_LEFT:
  assumes BIJ: "bij_betw f A A'" and SUB: "B \ A"
  shows "(inv_into A f)`(f ` B) = B"
  using assms unfolding bij_betw_def using inv_into_image_cancel by force

(*1*)lemma bij_betw_inv_into_LEFT_RIGHT:
  assumes BIJ: "bij_betw f A A'" and SUB: "B \ A" and
    IM: "f ` B = B'"
  shows "(inv_into A f) ` B' = B"
  using assms bij_betw_inv_into_LEFT[of f A A' B] by fast

subsection \<open>Other facts\<close>

(*3*)lemma atLeastLessThan_injective:
  assumes "{0 ..< m::nat} = {0 ..< n}"
  shows "m = n"
  using assms atLeast0LessThan by force

(*2*)lemma atLeastLessThan_injective2:
  "bij_betw f {0 ..< m::nat} {0 ..< n} \ m = n"
  using bij_betw_same_card by fastforce

(*2*)lemma atLeastLessThan_less_eq:
  "({0.. {0.. n)"
  by auto

(*2*)lemma atLeastLessThan_less_eq2:
  assumes "inj_on f {0..<(m::nat)}" "f ` {0.. {0..
  shows "m \ n"
  by (metis assms card_inj_on_le card_lessThan finite_lessThan lessThan_atLeast0)

(* unused *)
(*3*)lemma atLeastLessThan_less:
  "({0..
  by auto

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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.