2014-12-22 20:33:29 +00:00
|
|
|
|
/-
|
2015-04-06 01:52:13 +00:00
|
|
|
|
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
2014-12-22 20:33:29 +00:00
|
|
|
|
Author: Jeremy Avigad, Leonardo de Moura
|
|
|
|
|
-/
|
2015-08-09 06:18:20 +00:00
|
|
|
|
import logic.connectives logic.identities algebra.binary
|
2015-07-25 17:38:24 +00:00
|
|
|
|
open eq.ops binary
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition set (X : Type) := X → Prop
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2014-07-27 20:18:33 +00:00
|
|
|
|
namespace set
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
variable {X : Type}
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- membership and subset -/
|
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition mem (x : X) (a : set X) := a x
|
2015-09-30 15:06:31 +00:00
|
|
|
|
infix ∈ := mem
|
2015-05-08 02:52:46 +00:00
|
|
|
|
notation a ∉ b := ¬ mem a b
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
|
2015-04-05 14:12:27 +00:00
|
|
|
|
funext (take x, propext (H x))
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b
|
2015-09-30 15:06:31 +00:00
|
|
|
|
infix ⊆ := subset
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition superset (s t : set X) : Prop := t ⊆ s
|
2015-09-30 15:06:31 +00:00
|
|
|
|
infix ⊇ := superset
|
2015-08-10 01:18:25 +00:00
|
|
|
|
|
2015-06-04 08:51:34 +00:00
|
|
|
|
theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
|
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem subset.trans {a b c : set X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
|
2015-06-04 08:51:34 +00:00
|
|
|
|
take x, assume ax, subbc (subab ax)
|
|
|
|
|
|
2015-07-25 17:38:24 +00:00
|
|
|
|
theorem subset.antisymm {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
|
2015-06-17 16:53:50 +00:00
|
|
|
|
|
2015-07-25 17:38:24 +00:00
|
|
|
|
-- an alterantive name
|
|
|
|
|
theorem eq_of_subset_of_subset {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
|
|
|
|
|
subset.antisymm h₁ h₂
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_of_subset_of_mem {s₁ s₂ : set X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
|
|
|
|
|
assume h₁ h₂, h₁ _ h₂
|
|
|
|
|
|
|
|
|
|
/- strict subset -/
|
|
|
|
|
|
2015-06-17 16:53:50 +00:00
|
|
|
|
definition strict_subset (a b : set X) := a ⊆ b ∧ a ≠ b
|
2015-09-30 15:06:31 +00:00
|
|
|
|
infix ` ⊂ `:50 := strict_subset
|
2015-06-17 16:53:50 +00:00
|
|
|
|
|
|
|
|
|
theorem strict_subset.irrefl (a : set X) : ¬ a ⊂ a :=
|
|
|
|
|
assume h, absurd rfl (and.elim_right h)
|
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- bounded quantification -/
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
abbreviation bounded_forall (a : set X) (P : X → Prop) := ∀⦃x⦄, x ∈ a → P x
|
2015-09-30 23:52:34 +00:00
|
|
|
|
notation `forallb` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_forall a r
|
|
|
|
|
notation `∀₀` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_forall a r
|
2015-04-05 16:36:54 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
abbreviation bounded_exists (a : set X) (P : X → Prop) := ∃⦃x⦄, x ∈ a ∧ P x
|
2015-09-30 23:52:34 +00:00
|
|
|
|
notation `existsb` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_exists a r
|
|
|
|
|
notation `∃₀` binders `∈` a `, ` r:(scoped:1 P, P) := bounded_exists a r
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem bounded_exists.intro {P : X → Prop} {s : set X} {x : X} (xs : x ∈ s) (Px : P x) :
|
|
|
|
|
∃₀ x ∈ s, P x :=
|
|
|
|
|
exists.intro x (and.intro xs Px)
|
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- empty set -/
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition empty : set X := λx, false
|
2014-08-22 23:36:47 +00:00
|
|
|
|
notation `∅` := empty
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) :=
|
2015-03-01 16:23:39 +00:00
|
|
|
|
assume H : x ∈ ∅, H
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl
|
|
|
|
|
|
2015-07-25 17:38:24 +00:00
|
|
|
|
theorem eq_empty_of_forall_not_mem {s : set X} (H : ∀ x, x ∉ s) : s = ∅ :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, iff.intro
|
2015-07-25 17:38:24 +00:00
|
|
|
|
(assume xs, absurd xs (H x))
|
|
|
|
|
(assume xe, absurd xe !not_mem_empty))
|
|
|
|
|
|
|
|
|
|
theorem empty_subset (s : set X) : ∅ ⊆ s :=
|
|
|
|
|
take x, assume H, false.elim H
|
|
|
|
|
|
|
|
|
|
theorem eq_empty_of_subset_empty {s : set X} (H : s ⊆ ∅) : s = ∅ :=
|
|
|
|
|
subset.antisymm H (empty_subset s)
|
|
|
|
|
|
|
|
|
|
theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ :=
|
|
|
|
|
iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
|
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- universal set -/
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
definition univ : set X := λx, true
|
|
|
|
|
|
|
|
|
|
theorem mem_univ (x : X) : x ∈ univ := trivial
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_univ_iff (x : X) : x ∈ univ ↔ true := !iff.refl
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem mem_univ_eq (x : X) : x ∈ univ = true := rfl
|
|
|
|
|
|
2015-06-17 16:53:50 +00:00
|
|
|
|
theorem empty_ne_univ [h : inhabited X] : (empty : set X) ≠ univ :=
|
|
|
|
|
assume H : empty = univ,
|
|
|
|
|
absurd (mem_univ (inhabited.value h)) (eq.rec_on H (not_mem_empty _))
|
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem subset_univ (s : set X) : s ⊆ univ := λ x H, trivial
|
|
|
|
|
|
|
|
|
|
theorem eq_univ_of_univ_subset {s : set X} (H : univ ⊆ s) : s = univ :=
|
|
|
|
|
eq_of_subset_of_subset (subset_univ s) H
|
|
|
|
|
|
|
|
|
|
theorem eq_univ_of_forall {s : set X} (H : ∀ x, x ∈ s) : s = univ :=
|
|
|
|
|
ext (take x, iff.intro (assume H', trivial) (assume H', H x))
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
/- union -/
|
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition union (a b : set X) : set X := λx, x ∈ a ∨ x ∈ b
|
2015-05-08 02:52:46 +00:00
|
|
|
|
notation a ∪ b := union a b
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_union_left {x : X} {a : set X} (b : set X) : x ∈ a → x ∈ a ∪ b :=
|
|
|
|
|
assume h, or.inl h
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_union_right {x : X} {b : set X} (a : set X) : x ∈ b → x ∈ a ∪ b :=
|
|
|
|
|
assume h, or.inr h
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_unionl {x : X} {a b : set X} : x ∈ a → x ∈ a ∪ b :=
|
2015-08-09 06:18:20 +00:00
|
|
|
|
assume h, or.inl h
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_unionr {x : X} {a b : set X} : x ∈ b → x ∈ a ∪ b :=
|
2015-08-09 06:18:20 +00:00
|
|
|
|
assume h, or.inr h
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_or_mem_of_mem_union {x : X} {a b : set X} (H : x ∈ a ∪ b) : x ∈ a ∨ x ∈ b := H
|
|
|
|
|
|
|
|
|
|
theorem mem_union.elim {x : X} {a b : set X} {P : Prop}
|
|
|
|
|
(H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P :=
|
|
|
|
|
or.elim H₁ H₂ H₃
|
|
|
|
|
|
|
|
|
|
theorem mem_union_iff (x : X) (a b : set X) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b := !iff.refl
|
|
|
|
|
|
|
|
|
|
theorem mem_union_eq (x : X) (a b : set X) : x ∈ a ∪ b = (x ∈ a ∨ x ∈ b) := rfl
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem union_self (a : set X) : a ∪ a = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !or_self)
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
|
|
|
|
theorem union_empty (a : set X) : a ∪ ∅ = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !or_false)
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
|
|
|
|
theorem empty_union (a : set X) : ∅ ∪ a = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !false_or)
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
|
|
|
|
theorem union.comm (a b : set X) : a ∪ b = b ∪ a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, or.comm)
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
2015-06-17 16:53:50 +00:00
|
|
|
|
theorem union.assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, or.assoc)
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-07-25 17:38:24 +00:00
|
|
|
|
theorem union.left_comm (s₁ s₂ s₃ : set X) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
|
|
|
|
|
!left_comm union.comm union.assoc s₁ s₂ s₃
|
|
|
|
|
|
|
|
|
|
theorem union.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
|
|
|
|
|
!right_comm union.comm union.assoc s₁ s₂ s₃
|
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem subset_union_left (s t : set X) : s ⊆ s ∪ t := λ x H, or.inl H
|
|
|
|
|
|
|
|
|
|
theorem subset_union_right (s t : set X) : t ⊆ s ∪ t := λ x H, or.inr H
|
|
|
|
|
|
|
|
|
|
theorem union_subset {s t r : set X} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ r :=
|
|
|
|
|
λ x xst, or.elim xst (λ xs, sr xs) (λ xt, tr xt)
|
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- intersection -/
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition inter (a b : set X) : set X := λx, x ∈ a ∧ x ∈ b
|
2014-10-21 21:08:07 +00:00
|
|
|
|
notation a ∩ b := inter a b
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_inter_iff (x : X) (a b : set X) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b := !iff.refl
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
|
|
|
|
theorem mem_inter_eq (x : X) (a b : set X) : x ∈ a ∩ b = (x ∈ a ∧ x ∈ b) := rfl
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_inter {x : X} {a b : set X} (Ha : x ∈ a) (Hb : x ∈ b) : x ∈ a ∩ b :=
|
|
|
|
|
and.intro Ha Hb
|
|
|
|
|
|
|
|
|
|
theorem mem_of_mem_inter_left {x : X} {a b : set X} (H : x ∈ a ∩ b) : x ∈ a :=
|
|
|
|
|
and.left H
|
|
|
|
|
|
|
|
|
|
theorem mem_of_mem_inter_right {x : X} {a b : set X} (H : x ∈ a ∩ b) : x ∈ b :=
|
|
|
|
|
and.right H
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter_self (a : set X) : a ∩ a = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and_self)
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter_empty (a : set X) : a ∩ ∅ = ∅ :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and_false)
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem empty_inter (a : set X) : ∅ ∩ a = ∅ :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !false_and)
|
2015-04-05 14:12:27 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter.comm (a b : set X) : a ∩ b = b ∩ a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and.comm)
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter.assoc (a b c : set X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and.assoc)
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-07-25 17:38:24 +00:00
|
|
|
|
theorem inter.left_comm (s₁ s₂ s₃ : set X) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
|
|
|
|
|
!left_comm inter.comm inter.assoc s₁ s₂ s₃
|
|
|
|
|
|
|
|
|
|
theorem inter.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
|
|
|
|
|
!right_comm inter.comm inter.assoc s₁ s₂ s₃
|
|
|
|
|
|
2015-06-17 16:53:50 +00:00
|
|
|
|
theorem inter_univ (a : set X) : a ∩ univ = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and_true)
|
2015-06-17 16:53:50 +00:00
|
|
|
|
|
|
|
|
|
theorem univ_inter (a : set X) : univ ∩ a = a :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !true_and)
|
|
|
|
|
|
|
|
|
|
theorem inter_subset_left (s t : set X) : s ∩ t ⊆ s := λ x H, and.left H
|
|
|
|
|
|
|
|
|
|
theorem inter_subset_right (s t : set X) : s ∩ t ⊆ t := λ x H, and.right H
|
|
|
|
|
|
|
|
|
|
theorem subset_inter {s t r : set X} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t :=
|
|
|
|
|
λ x xr, and.intro (rs xr) (rt xr)
|
2015-06-17 16:53:50 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
/- distributivity laws -/
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter.distrib_left (s t u : set X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and.left_distrib)
|
2014-07-27 20:18:33 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem inter.distrib_right (s t u : set X) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !and.right_distrib)
|
2014-08-26 05:54:44 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem union.distrib_left (s t u : set X) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !or.left_distrib)
|
2015-03-01 16:23:39 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem union.distrib_right (s t u : set X) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, !or.right_distrib)
|
2014-08-22 23:36:47 +00:00
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- set-builder notation -/
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
-- {x : X | P}
|
2015-10-16 19:32:44 +00:00
|
|
|
|
definition set_of (P : X → Prop) : set X := P
|
2015-09-30 15:06:31 +00:00
|
|
|
|
notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r
|
2015-04-05 16:36:54 +00:00
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
-- {x ∈ s | P}
|
2015-08-08 22:10:44 +00:00
|
|
|
|
definition sep (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
|
2015-09-30 15:06:31 +00:00
|
|
|
|
notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
|
2015-05-08 02:52:46 +00:00
|
|
|
|
|
2015-08-06 20:43:18 +00:00
|
|
|
|
/- insert -/
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
|
2015-08-06 20:43:18 +00:00
|
|
|
|
|
|
|
|
|
-- '{x, y, z}
|
2015-09-30 15:06:31 +00:00
|
|
|
|
notation `'{`:max a:(foldr `, ` (x b, insert x b) ∅) `}`:0 := a
|
2015-04-05 16:36:54 +00:00
|
|
|
|
|
2015-08-06 20:43:18 +00:00
|
|
|
|
theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a :=
|
|
|
|
|
take y, assume ys, or.inr ys
|
|
|
|
|
|
2015-08-09 06:18:20 +00:00
|
|
|
|
theorem mem_insert (x : X) (s : set X) : x ∈ insert x s :=
|
|
|
|
|
or.inl rfl
|
|
|
|
|
|
|
|
|
|
theorem mem_insert_of_mem {x : X} {s : set X} (y : X) : x ∈ s → x ∈ insert y s :=
|
|
|
|
|
assume h, or.inr h
|
|
|
|
|
|
|
|
|
|
theorem eq_or_mem_of_mem_insert {x a : X} {s : set X} : x ∈ insert a s → x = a ∨ x ∈ s :=
|
|
|
|
|
assume h, h
|
|
|
|
|
|
|
|
|
|
theorem mem_of_mem_insert_of_ne {x a : X} {s : set X} (xin : x ∈ insert a s) : x ≠ a → x ∈ s :=
|
|
|
|
|
or_resolve_right (eq_or_mem_of_mem_insert xin)
|
|
|
|
|
|
|
|
|
|
theorem mem_insert_eq (x a : X) (s : set X) : x ∈ insert a s = (x = a ∨ x ∈ s) :=
|
|
|
|
|
propext (iff.intro !eq_or_mem_of_mem_insert
|
|
|
|
|
(or.rec (λH', (eq.substr H' !mem_insert)) !mem_insert_of_mem))
|
|
|
|
|
|
|
|
|
|
theorem insert_eq_of_mem {a : X} {s : set X} (H : a ∈ s) : insert a s = s :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (λ x, eq.substr (mem_insert_eq x a s)
|
2015-08-09 06:18:20 +00:00
|
|
|
|
(or_iff_right_of_imp (λH1, eq.substr H1 H)))
|
|
|
|
|
|
|
|
|
|
theorem insert.comm (x y : X) (s : set X) : insert x (insert y s) = insert y (insert x s) :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take a, by rewrite [*mem_insert_eq, propext !or.left_comm])
|
2015-08-09 06:18:20 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
/- singleton -/
|
2015-08-09 06:18:20 +00:00
|
|
|
|
|
2015-08-10 01:18:25 +00:00
|
|
|
|
theorem mem_singleton_iff (a b : X) : a ∈ '{b} ↔ a = b :=
|
|
|
|
|
iff.intro
|
|
|
|
|
(assume ainb, or.elim ainb (λ aeqb, aeqb) (λ f, false.elim f))
|
|
|
|
|
(assume aeqb, or.inl aeqb)
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_singleton (a : X) : a ∈ '{a} := !mem_insert
|
|
|
|
|
|
|
|
|
|
theorem eq_of_mem_singleton {x y : X} : x ∈ insert y ∅ → x = y :=
|
|
|
|
|
assume h, or.elim (eq_or_mem_of_mem_insert h)
|
|
|
|
|
(suppose x = y, this)
|
|
|
|
|
(suppose x ∈ ∅, absurd this !not_mem_empty)
|
|
|
|
|
|
2015-08-08 22:10:44 +00:00
|
|
|
|
/- separation -/
|
2015-08-04 20:47:16 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_sep {s : set X} {P : X → Prop} {x : X} (xs : x ∈ s) (Px : P x) : x ∈ {x ∈ s | P x} :=
|
|
|
|
|
and.intro xs Px
|
|
|
|
|
|
2015-08-08 22:10:44 +00:00
|
|
|
|
theorem eq_sep_of_subset {s t : set X} (ssubt : s ⊆ t) : s = {x ∈ t | x ∈ s} :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, iff.intro
|
2015-08-04 20:47:16 +00:00
|
|
|
|
(suppose x ∈ s, and.intro (ssubt this) this)
|
|
|
|
|
(suppose x ∈ {x ∈ t | x ∈ s}, and.right this))
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_sep_iff {s : set X} {P : X → Prop} {x : X} : x ∈ {x ∈ s | P x} ↔ x ∈ s ∧ P x :=
|
|
|
|
|
!iff.refl
|
|
|
|
|
|
2015-09-25 03:38:52 +00:00
|
|
|
|
theorem sep_subset (s : set X) (P : X → Prop) : {x ∈ s | P x} ⊆ s :=
|
|
|
|
|
take x, assume H, and.left H
|
|
|
|
|
|
2015-08-27 18:26:21 +00:00
|
|
|
|
/- complement -/
|
|
|
|
|
|
|
|
|
|
definition complement (s : set X) : set X := {x | x ∉ s}
|
|
|
|
|
prefix `-` := complement
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_comp {s : set X} {x : X} (H : x ∉ s) : x ∈ -s := H
|
|
|
|
|
|
|
|
|
|
theorem not_mem_of_mem_comp {s : set X} {x : X} (H : x ∈ -s) : x ∉ s := H
|
2015-08-27 18:26:21 +00:00
|
|
|
|
|
2015-09-25 03:38:52 +00:00
|
|
|
|
theorem mem_comp_iff (s : set X) (x : X) : x ∈ -s ↔ x ∉ s := !iff.refl
|
|
|
|
|
|
|
|
|
|
theorem inter_comp_self (s : set X) : s ∩ -s = ∅ :=
|
|
|
|
|
ext (take x, !and_not_self_iff)
|
|
|
|
|
|
|
|
|
|
theorem comp_inter_self (s : set X) : -s ∩ s = ∅ :=
|
|
|
|
|
ext (take x, !not_and_self_iff)
|
|
|
|
|
|
|
|
|
|
/- some classical identities -/
|
2015-08-27 18:26:21 +00:00
|
|
|
|
|
|
|
|
|
section
|
|
|
|
|
open classical
|
|
|
|
|
|
|
|
|
|
theorem union_eq_comp_comp_inter_comp (s t : set X) : s ∪ t = -(-s ∩ -t) :=
|
|
|
|
|
ext (take x, !or_iff_not_and_not)
|
|
|
|
|
|
|
|
|
|
theorem inter_eq_comp_comp_union_comp (s t : set X) : s ∩ t = -(-s ∪ -t) :=
|
|
|
|
|
ext (take x, !and_iff_not_or_not)
|
2015-09-25 03:38:52 +00:00
|
|
|
|
|
|
|
|
|
theorem union_comp_self (s : set X) : s ∪ -s = univ :=
|
|
|
|
|
ext (take x, !or_not_self_iff)
|
|
|
|
|
|
|
|
|
|
theorem comp_union_self (s : set X) : -s ∪ s = univ :=
|
|
|
|
|
ext (take x, !not_or_self_iff)
|
2015-08-27 18:26:21 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
/- set difference -/
|
|
|
|
|
|
|
|
|
|
definition diff (s t : set X) : set X := {x ∈ s | x ∉ t}
|
|
|
|
|
infix `\`:70 := diff
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_diff {s t : set X} {x : X} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t :=
|
|
|
|
|
and.intro H1 H2
|
|
|
|
|
|
2015-05-08 02:52:46 +00:00
|
|
|
|
theorem mem_of_mem_diff {s t : set X} {x : X} (H : x ∈ s \ t) : x ∈ s :=
|
|
|
|
|
and.left H
|
|
|
|
|
|
|
|
|
|
theorem not_mem_of_mem_diff {s t : set X} {x : X} (H : x ∈ s \ t) : x ∉ t :=
|
|
|
|
|
and.right H
|
|
|
|
|
|
|
|
|
|
theorem mem_diff_iff (s t : set X) (x : X) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t := !iff.refl
|
|
|
|
|
|
|
|
|
|
theorem mem_diff_eq (s t : set X) (x : X) : x ∈ s \ t = (x ∈ s ∧ x ∉ t) := rfl
|
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem diff_eq (s t : set X) : s \ t = s ∩ -t := rfl
|
|
|
|
|
|
2015-08-07 21:01:28 +00:00
|
|
|
|
theorem union_diff_cancel {s t : set X} [dec : Π x, decidable (x ∈ s)] (H : s ⊆ t) : s ∪ (t \ s) = t :=
|
2015-08-10 01:18:25 +00:00
|
|
|
|
ext (take x, iff.intro
|
2015-08-07 21:01:28 +00:00
|
|
|
|
(assume H1 : x ∈ s ∪ (t \ s), or.elim H1 (assume H2, !H H2) (assume H2, and.left H2))
|
|
|
|
|
(assume H1 : x ∈ t,
|
2015-08-08 00:53:30 +00:00
|
|
|
|
decidable.by_cases
|
2015-08-07 21:01:28 +00:00
|
|
|
|
(suppose x ∈ s, or.inl this)
|
|
|
|
|
(suppose x ∉ s, or.inr (and.intro H1 this))))
|
|
|
|
|
|
2015-09-25 03:38:52 +00:00
|
|
|
|
theorem diff_subset (s t : set X) : s \ t ⊆ s := inter_subset_left s _
|
|
|
|
|
|
2015-08-05 02:36:10 +00:00
|
|
|
|
/- powerset -/
|
|
|
|
|
|
|
|
|
|
definition powerset (s : set X) : set (set X) := {x : set X | x ⊆ s}
|
2015-08-13 16:04:00 +00:00
|
|
|
|
prefix `𝒫`:100 := powerset
|
2015-08-05 02:36:10 +00:00
|
|
|
|
|
2015-09-03 00:51:23 +00:00
|
|
|
|
theorem mem_powerset {x s : set X} (H : x ⊆ s) : x ∈ 𝒫 s := H
|
|
|
|
|
|
|
|
|
|
theorem subset_of_mem_powerset {x s : set X} (H : x ∈ 𝒫 s) : x ⊆ s := H
|
|
|
|
|
|
|
|
|
|
theorem mem_powerset_iff (x s : set X) : x ∈ 𝒫 s ↔ x ⊆ s := !iff.refl
|
|
|
|
|
|
2015-04-05 16:36:54 +00:00
|
|
|
|
/- large unions -/
|
|
|
|
|
|
|
|
|
|
section
|
|
|
|
|
variables {I : Type}
|
|
|
|
|
variable a : set I
|
2015-05-08 02:52:46 +00:00
|
|
|
|
variable b : I → set X
|
|
|
|
|
variable C : set (set X)
|
|
|
|
|
|
|
|
|
|
definition Inter : set X := {x : X | ∀i, x ∈ b i}
|
|
|
|
|
definition bInter : set X := {x : X | ∀₀ i ∈ a, x ∈ b i}
|
|
|
|
|
definition sInter : set X := {x : X | ∀₀ c ∈ C, x ∈ c}
|
|
|
|
|
definition Union : set X := {x : X | ∃i, x ∈ b i}
|
|
|
|
|
definition bUnion : set X := {x : X | ∃₀ i ∈ a, x ∈ b i}
|
|
|
|
|
definition sUnion : set X := {x : X | ∃₀ c ∈ C, x ∈ c}
|
2015-04-05 16:36:54 +00:00
|
|
|
|
|
|
|
|
|
-- TODO: need notation for these
|
2015-09-25 03:38:52 +00:00
|
|
|
|
|
|
|
|
|
theorem Union_subset {b : I → set X} {c : set X} (H : ∀ i, b i ⊆ c) : Union b ⊆ c :=
|
|
|
|
|
take x,
|
|
|
|
|
suppose x ∈ Union b,
|
|
|
|
|
obtain i (Hi : x ∈ b i), from this,
|
|
|
|
|
show x ∈ c, from H i Hi
|
2015-11-26 16:18:51 +00:00
|
|
|
|
|
|
|
|
|
theorem sUnion_insert (s : set (set X)) (a : set X) :
|
|
|
|
|
sUnion (insert a s) = a ∪ sUnion s :=
|
|
|
|
|
ext (take x, iff.intro
|
|
|
|
|
(suppose x ∈ sUnion (insert a s),
|
|
|
|
|
obtain c [(cias : c ∈ insert a s) (xc : x ∈ c)], from this,
|
|
|
|
|
or.elim cias
|
|
|
|
|
(suppose c = a,
|
|
|
|
|
show x ∈ a ∪ sUnion s, from or.inl (this ▸ xc))
|
|
|
|
|
(suppose c ∈ s,
|
|
|
|
|
show x ∈ a ∪ sUnion s, from or.inr (exists.intro c (and.intro this xc))))
|
|
|
|
|
(suppose x ∈ a ∪ sUnion s,
|
|
|
|
|
or.elim this
|
|
|
|
|
(suppose x ∈ a,
|
|
|
|
|
have a ∈ insert a s, from or.inl rfl,
|
|
|
|
|
show x ∈ sUnion (insert a s), from exists.intro a (and.intro this `x ∈ a`))
|
|
|
|
|
(suppose x ∈ sUnion s,
|
|
|
|
|
obtain c [(cs : c ∈ s) (xc : x ∈ c)], from this,
|
|
|
|
|
have c ∈ insert a s, from or.inr cs,
|
|
|
|
|
show x ∈ sUnion (insert a s), from exists.intro c (and.intro this `x ∈ c`))))
|
2015-04-05 16:36:54 +00:00
|
|
|
|
end
|
|
|
|
|
|
2014-08-07 23:59:08 +00:00
|
|
|
|
end set
|