From 1cb3e5c658531e9e581612b126d1ef5db6ac7a3a Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 26 Jun 2017 17:39:40 +0100 Subject: [PATCH] change terminology set -> property --- algebra/subgroup.hlean | 78 ++++++++--------- property.hlean | 183 ++++++++++++++++++++++++++++++++++++++++ set.hlean | 186 ----------------------------------------- 3 files changed, 222 insertions(+), 225 deletions(-) create mode 100644 property.hlean delete mode 100644 set.hlean diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean index bd6ef98..44e3c42 100644 --- a/algebra/subgroup.hlean +++ b/algebra/subgroup.hlean @@ -5,9 +5,9 @@ Authors: Floris van Doorn, Egbert Rijke, Jeremy Avigad Basic concepts of group theory -/ -import algebra.group_theory ..move_to_lib ..set +import algebra.group_theory ..move_to_lib ..property -open eq algebra is_trunc sigma sigma.ops prod trunc set +open eq algebra is_trunc sigma sigma.ops prod trunc property namespace group @@ -17,7 +17,7 @@ namespace group group G to be a family of mere propositions over (the underlying type of) G, closed under the constants and operations --/ - structure is_subgroup [class] (G : Group) (H : set G) : Type := + structure is_subgroup [class] (G : Group) (H : property G) : Type := (one_mem : 1 ∈ H) (mul_mem : Π{g h}, g ∈ H → h ∈ H → g * h ∈ H) (inv_mem : Π{g}, g ∈ H → g⁻¹ ∈ H) @@ -50,14 +50,14 @@ namespace group is_subgroup H (image f) := begin fapply is_subgroup.mk, - -- subset contains 1 + -- subproperty contains 1 { fapply image.mk, exact 1, apply respect_one}, - -- subset is closed under multiplication + -- subproperty is closed under multiplication { intro h h', intro u v, induction u with x p, induction v with y q, induction p, induction q, apply image.mk (x * y), apply respect_mul}, - -- subset is closed under inverses + -- subproperty is closed under inverses { intro g, intro t, induction t with x p, induction p, apply image.mk x⁻¹, apply respect_inv } end @@ -66,8 +66,8 @@ namespace group variables {G₁ G₂ : Group} - -- TODO: maybe define this in more generality for pointed sets? - definition kernel [constructor] (φ : G₁ →g G₂) : set G₁ := { g | trunctype.mk (φ g = 1) _} + -- TODO: maybe define this in more generality for pointed propertys? + definition kernel [constructor] (φ : G₁ →g G₂) : property G₁ := { g | trunctype.mk (φ g = 1) _} theorem mul_mem_kernel (φ : G₁ →g G₂) (g h : G₁) (H₁ : g ∈ kernel φ) (H₂ : h ∈ kernel φ) : g * h ∈ kernel φ := calc @@ -103,10 +103,10 @@ namespace group /-- Next, we formalize some aspects of normal subgroups. Recall that a normal subgroup H of a group G is a subgroup which is invariant under all inner automorophisms on G. --/ - definition is_normal [constructor] (G : Group) (N : set G) : Prop := + definition is_normal [constructor] (G : Group) (N : property G) : Prop := trunctype.mk (Π{g} h, g ∈ N → h * g * h⁻¹ ∈ N) _ - structure is_normal_subgroup [class] (G : Group) (N : set G) extends is_subgroup G N := + structure is_normal_subgroup [class] (G : Group) (N : property G) extends is_subgroup G N := (is_normal : is_normal G N) abbreviation subgroup_one_mem [unfold 2] := @is_subgroup.one_mem @@ -115,14 +115,14 @@ namespace group abbreviation subgroup_is_normal [unfold 2] := @is_normal_subgroup.is_normal section - variables {G G' G₁ G₂ G₃ : Group} {H N : set G} [is_subgroup G H] + variables {G G' G₁ G₂ G₃ : Group} {H N : property G} [is_subgroup G H] [is_normal_subgroup G N] {g g' h h' k : G} {A B : AbGroup} theorem is_normal_subgroup' (h : G) (r : g ∈ N) : h⁻¹ * g * h ∈ N := inv_inv h ▸ subgroup_is_normal N h⁻¹ r - definition is_normal_subgroup_ab.{u} [constructor] {C : set A} (subgrpA : is_subgroup A C) + definition is_normal_subgroup_ab.{u} [constructor] {C : property A} (subgrpA : is_subgroup A C) : is_normal_subgroup A C := ⦃ is_normal_subgroup, subgrpA, is_normal := abstract begin @@ -164,7 +164,7 @@ section end -- this is just (Σ(g : G), H g), but only defined if (H g) is a prop - definition sg {G : Group} (H : set G) : Type := {g : G | g ∈ H} + definition sg {G : Group} (H : property G) : Type := {g : G | g ∈ H} local attribute sg [reducible] definition subgroup_one [constructor] : sg H := ⟨one, subgroup_one_mem H⟩ @@ -192,7 +192,7 @@ section theorem subgroup_mul_left_inv (g : sg H) : g⁻¹ * g = 1 := subtype_eq !mul.left_inv - theorem subgroup_mul_comm {G : AbGroup} {H : set G} [subgrpH : is_subgroup G H] (g h : sg H) + theorem subgroup_mul_comm {G : AbGroup} {H : property G} [subgrpH : is_subgroup G H] (g h : sg H) : subgroup_mul g h = subgroup_mul h g := subtype_eq !mul.comm @@ -209,11 +209,11 @@ section variable {H} - definition ab_group_sg [constructor] {G : AbGroup} (H : set G) [is_subgroup G H] + definition ab_group_sg [constructor] {G : AbGroup} (H : property G) [is_subgroup G H] : ab_group (sg H) := ⦃ab_group, (group_sg H), mul_comm := subgroup_mul_comm⦄ - definition ab_subgroup [constructor] {G : AbGroup} (H : set G) [is_subgroup G H] + definition ab_subgroup [constructor] {G : AbGroup} (H : property G) [is_subgroup G H] : AbGroup := AbGroup.mk _ (ab_group_sg H) @@ -221,7 +221,7 @@ section definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel f) - definition incl_of_subgroup [constructor] {G : Group} (H : set G) [is_subgroup G H] : + definition incl_of_subgroup [constructor] {G : Group} (H : property G) [is_subgroup G H] : subgroup H →g G := begin fapply homomorphism.mk, @@ -231,7 +231,7 @@ section intro g h, reflexivity end - definition is_embedding_incl_of_subgroup {G : Group} (H : set G) [is_subgroup G H] : + definition is_embedding_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H] : is_embedding (incl_of_subgroup H) := begin fapply function.is_embedding_of_is_injective, @@ -249,20 +249,20 @@ section fapply is_embedding_incl_of_subgroup, end - definition is_subgroup_of_subgroup {G : Group} {H1 H2 : set G} [is_subgroup G H1] + definition is_subgroup_of_subgroup {G : Group} {H1 H2 : property G} [is_subgroup G H1] [is_subgroup G H2] (hyp : Π (g : G), g ∈ H1 → g ∈ H2) : is_subgroup (subgroup H2) {h | incl_of_subgroup H2 h ∈ H1} := is_subgroup.mk (subgroup_one_mem H1) (begin intros g h p q, - apply mem_set_of, - apply subgroup_mul_mem (of_mem_set_of p) (of_mem_set_of q), + apply mem_property_of, + apply subgroup_mul_mem (of_mem_property_of p) (of_mem_property_of q), end) (begin intros h p, - apply mem_set_of, - apply subgroup_inv_mem (of_mem_set_of p) + apply mem_property_of, + apply subgroup_inv_mem (of_mem_property_of p) end) definition Image {G H : Group} (f : G →g H) : Group := @@ -306,7 +306,7 @@ definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A → exact is_equiv_surjection_ab_image_incl f H end - definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g subgroup K := + definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : property H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g subgroup K := begin fapply homomorphism.mk, intro g, @@ -316,14 +316,14 @@ definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A → intro g h, apply subtype_eq, esimp, apply respect_mul end -definition hom_factors_through_lift {G H : Group} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : +definition hom_factors_through_lift {G H : Group} (f : G →g H) (K : property H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : f = incl_of_subgroup K ∘g hom_lift f K Hyp := begin fapply homomorphism_eq, reflexivity end -definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g ab_subgroup K := +definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : property H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : G →g ab_subgroup K := begin fapply homomorphism.mk, intro g, @@ -333,7 +333,7 @@ definition ab_hom_lift [constructor] {G H : AbGroup} (f : G →g H) (K : set H) intro g h, apply subtype_eq, apply respect_mul, end -definition ab_hom_factors_through_lift {G H : AbGroup} (f : G →g H) (K : set H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : +definition ab_hom_factors_through_lift {G H : AbGroup} (f : G →g H) (K : property H) [is_subgroup H K] (Hyp : Π (g : G), K (f g)) : f = incl_of_subgroup K ∘g hom_lift f K Hyp := begin fapply homomorphism_eq, @@ -438,8 +438,8 @@ end intro x, induction x with b p, induction p with x, induction p, reflexivity end - variables {G H K : Group} {R : set G} [is_subgroup G R] - {S : set H} [is_subgroup H S] {T : set K} [is_subgroup K T] + variables {G H K : Group} {R : property G} [is_subgroup G R] + {S : property H} [is_subgroup H S] {T : property K} [is_subgroup K T] open function definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S) @@ -460,8 +460,8 @@ end end definition ab_subgroup_functor [constructor] {G H : AbGroup} - {R : set G} [is_subgroup G R] - {S : set H} [is_subgroup H S] + {R : property G} [is_subgroup G R] + {S : property H} [is_subgroup H S] (φ : G →g H) (h : Πg, g ∈ R → φ g ∈ S) : ab_subgroup R →g ab_subgroup S := subgroup_functor φ h @@ -479,8 +479,8 @@ end intro g, induction g with g hg, reflexivity end - definition subgroup_functor_mul {G H : AbGroup} {R : set G} [subgroupR : is_subgroup G R] - {S : set H} [subgroupS : is_subgroup H S] + definition subgroup_functor_mul {G H : AbGroup} {R : property G} [subgroupR : is_subgroup G R] + {S : property H} [subgroupS : is_subgroup H S] (ψ φ : G →g H) (hψ : Πg, g ∈ R → ψ g ∈ S) (hφ : Πg, g ∈ R → φ g ∈ S) : homomorphism_mul (ab_subgroup_functor ψ hψ) (ab_subgroup_functor φ hφ) ~ ab_subgroup_functor (homomorphism_mul ψ φ) @@ -497,12 +497,12 @@ end exact subtype_eq (p g) end - definition subgroup_of_subgroup_incl {R S : set G} [is_subgroup G R] [is_subgroup G S] + definition subgroup_of_subgroup_incl {R S : property G} [is_subgroup G R] [is_subgroup G S] (H : Π (g : G), g ∈ R → g ∈ S) : subgroup R →g subgroup S := subgroup_functor (gid G) H - definition is_embedding_subgroup_of_subgroup_incl {R S : set G} [is_subgroup G R] [is_subgroup G S] + definition is_embedding_subgroup_of_subgroup_incl {R S : property G} [is_subgroup G R] [is_subgroup G S] (H : Π (g : G), g ∈ R -> g ∈ S) : is_embedding (subgroup_of_subgroup_incl H) := begin fapply is_embedding_of_is_injective, @@ -512,18 +512,18 @@ end unfold subgroup_of_subgroup_incl at p, exact ap pr1 p, end - definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S] + definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S] (H : Π (a : A), a ∈ R → a ∈ S) : ab_subgroup R →g ab_subgroup S := ab_subgroup_functor (gid A) H - definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S] + definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S] (H : Π (a : A), a ∈ R → a ∈ S) : is_embedding (ab_subgroup_of_subgroup_incl H) := begin fapply is_embedding_subgroup_of_subgroup_incl end - definition ab_subgroup_iso {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S] + definition ab_subgroup_iso {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S] (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) : ab_subgroup R ≃g ab_subgroup S := begin @@ -535,7 +535,7 @@ end intro r, induction r with a p, fapply subtype_eq, reflexivity end - definition ab_subgroup_iso_triangle {A : AbGroup} {R S : set A} [is_subgroup A R] [is_subgroup A S] + definition ab_subgroup_iso_triangle {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S] (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) : incl_of_subgroup R ~ incl_of_subgroup S ∘g ab_subgroup_iso H K := begin diff --git a/property.hlean b/property.hlean new file mode 100644 index 0000000..0b58c5d --- /dev/null +++ b/property.hlean @@ -0,0 +1,183 @@ +/- +Copyright (c) 2017 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jeremy Avigad +-/ +import types.trunc .logic +open funext eq trunc is_trunc logic + +definition property (X : Type) := X → Prop + +namespace property + +variable {X : Type} + +/- membership and subproperty -/ + +definition mem (x : X) (a : property X) := a x +infix ∈ := mem +notation a ∉ b := ¬ mem a b + +/-theorem ext {a b : property X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b := +eq_of_homotopy (take x, propext (H x)) +-/ + +definition subproperty (a b : property X) : Prop := Prop.mk (∀⦃x⦄, x ∈ a → x ∈ b) _ +infix ⊆ := subproperty + +definition superproperty (s t : property X) : Prop := t ⊆ s +infix ⊇ := superproperty + +theorem subproperty.refl (a : property X) : a ⊆ a := take x, assume H, H + +theorem subproperty.trans {a b c : property X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c := +take x, assume ax, subbc (subab ax) + +/- +theorem subproperty.antisymm {a b : property X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b := +ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb)) +-/ + +-- an alterantive name +/- +theorem eq_of_subproperty_of_subproperty {a b : property X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b := +subproperty.antisymm h₁ h₂ +-/ + +theorem mem_of_subproperty_of_mem {s₁ s₂ : property X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := +assume h₁ h₂, h₁ _ h₂ + +/- empty property -/ + +definition empty : property X := λx, false +notation `∅` := property.empty + +theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) := +assume H : x ∈ ∅, false.elim H + +theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl + +/- +theorem eq_empty_of_forall_not_mem {s : property X} (H : ∀ x, x ∉ s) : s = ∅ := +ext (take x, iff.intro + (assume xs, absurd xs (H x)) + (assume xe, absurd xe (not_mem_empty x))) +-/ + +theorem ne_empty_of_mem {s : property X} {x : X} (H : x ∈ s) : s ≠ ∅ := + begin intro Hs, rewrite Hs at H, apply not_mem_empty x H end + +theorem empty_subproperty (s : property X) : ∅ ⊆ s := +take x, assume H, false.elim H + +/-theorem eq_empty_of_subproperty_empty {s : property X} (H : s ⊆ ∅) : s = ∅ := +subproperty.antisymm H (empty_subproperty s) + +theorem subproperty_empty_iff (s : property X) : s ⊆ ∅ ↔ s = ∅ := +iff.intro eq_empty_of_subproperty_empty (take xeq, by rewrite xeq; apply subproperty.refl ∅) +-/ + +/- universal property -/ + +definition univ : property X := λx, true + +theorem mem_univ (x : X) : x ∈ univ := trivial + +theorem mem_univ_eq (x : X) : x ∈ univ = true := rfl + +theorem empty_ne_univ [h : inhabited X] : (empty : property X) ≠ univ := +assume H : empty = univ, +absurd (mem_univ (inhabited.value h)) (eq.rec_on H (not_mem_empty (arbitrary X))) + +theorem subproperty_univ (s : property X) : s ⊆ univ := λ x H, trivial + +/- +theorem eq_univ_of_univ_subproperty {s : property X} (H : univ ⊆ s) : s = univ := +eq_of_subproperty_of_subproperty (subproperty_univ s) H +-/ + +/- +theorem eq_univ_of_forall {s : property X} (H : ∀ x, x ∈ s) : s = univ := +ext (take x, iff.intro (assume H', trivial) (assume H', H x)) +-/ + +/- property-builder notation -/ + +-- {x : X | P} +definition property_of (P : X → Prop) : property X := P +notation `{` binder ` | ` r:(scoped:1 P, property_of P) `}` := r + +theorem mem_property_of {P : X → Prop} {a : X} (h : P a) : a ∈ {x | P x} := h + +theorem of_mem_property_of {P : X → Prop} {a : X} (h : a ∈ {x | P x}) : P a := h + +-- {x ∈ s | P} +definition sep (P : X → Prop) (s : property X) : property X := λx, x ∈ s ∧ P x +notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r + +/- insert -/ + +definition insert (x : X) (a : property X) : property X := {y : X | y = x ∨ y ∈ a} + +abbreviation insert_same_level.{u} := @insert.{u u} + +-- '{x, y, z} +notation `'{`:max a:(foldr `, ` (x b, insert_same_level x b) ∅) `}`:0 := a + +theorem subproperty_insert (x : X) (a : property X) : a ⊆ insert x a := +take y, assume ys, or.inr ys + +theorem mem_insert (x : X) (s : property X) : x ∈ insert x s := +or.inl rfl + +theorem mem_insert_of_mem {x : X} {s : property 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 : property X} : x ∈ insert a s → x = a ∨ x ∈ s := +assume h, h + +/- singleton -/ + +open trunc_index + +theorem mem_singleton_iff {X : Type} [is_set X] (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) + +theorem mem_singleton (a : X) : a ∈ '{a} := !mem_insert + +theorem eq_of_mem_singleton {X : Type} [is_set X] {x y : X} (h : x ∈ '{y}) : x = y := +or.elim (eq_or_mem_of_mem_insert h) + (suppose x = y, this) + (suppose x ∈ ∅, absurd this (not_mem_empty x)) + +theorem mem_singleton_of_eq {x y : X} (H : x = y) : x ∈ '{y} := +eq.symm H ▸ mem_singleton y + +/- +theorem insert_eq (x : X) (s : property X) : insert x s = '{x} ∪ s := +ext (take y, iff.intro + (suppose y ∈ insert x s, + or.elim this (suppose y = x, or.inl (or.inl this)) (suppose y ∈ s, or.inr this)) + (suppose y ∈ '{x} ∪ s, + or.elim this + (suppose y ∈ '{x}, or.inl (eq_of_mem_singleton this)) + (suppose y ∈ s, or.inr this))) +-/ + +/- +theorem pair_eq_singleton (a : X) : '{a, a} = '{a} := +by rewrite [insert_eq_of_mem !mem_singleton] +-/ +/- +theorem singleton_ne_empty (a : X) : '{a} ≠ ∅ := +begin + intro H, + apply not_mem_empty a, + rewrite -H, + apply mem_insert +end +-/ + +end property diff --git a/set.hlean b/set.hlean deleted file mode 100644 index 65be6df..0000000 --- a/set.hlean +++ /dev/null @@ -1,186 +0,0 @@ -/- -Copyright (c) 2017 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad --/ -import types.trunc .logic -open funext eq trunc is_trunc logic - -definition set (X : Type) := X → Prop - -namespace set - -variable {X : Type} - -/- membership and subset -/ - -definition mem (x : X) (a : set X) := a x -infix ∈ := mem -notation a ∉ b := ¬ mem a b - -/-theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b := -eq_of_homotopy (take x, propext (H x)) --/ - -definition subset (a b : set X) : Prop := Prop.mk (∀⦃x⦄, x ∈ a → x ∈ b) _ -infix ⊆ := subset - -definition superset (s t : set X) : Prop := t ⊆ s -infix ⊇ := superset - -theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H - -theorem subset.trans {a b c : set X} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c := -take x, assume ax, subbc (subab ax) - -/- -theorem subset.antisymm {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b := -ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb)) --/ - --- 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₂ --/ - -theorem mem_of_subset_of_mem {s₁ s₂ : set X} {a : X} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := -assume h₁ h₂, h₁ _ h₂ - -/- empty set -/ - -definition empty : set X := λx, false -notation `∅` := set.empty - -theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) := -assume H : x ∈ ∅, false.elim H - -theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl - -/- -theorem eq_empty_of_forall_not_mem {s : set X} (H : ∀ x, x ∉ s) : s = ∅ := -ext (take x, iff.intro - (assume xs, absurd xs (H x)) - (assume xe, absurd xe (not_mem_empty x))) --/ - -set_option formatter.hide_full_terms false - -theorem ne_empty_of_mem {s : set X} {x : X} (H : x ∈ s) : s ≠ ∅ := - begin intro Hs, rewrite Hs at H, apply not_mem_empty x H end - - -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 ∅) --/ - -/- universal set -/ - -definition univ : set X := λx, true - -theorem mem_univ (x : X) : x ∈ univ := trivial - -theorem mem_univ_eq (x : X) : x ∈ univ = true := rfl - -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 (arbitrary X))) - -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)) --/ - -/- set-builder notation -/ - --- {x : X | P} -definition set_of (P : X → Prop) : set X := P -notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r - -theorem mem_set_of {P : X → Prop} {a : X} (h : P a) : a ∈ {x | P x} := h - -theorem of_mem_set_of {P : X → Prop} {a : X} (h : a ∈ {x | P x}) : P a := h - --- {x ∈ s | P} -definition sep (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x -notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r - -/- insert -/ - -definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a} - -abbreviation insert_same_level.{u} := @insert.{u u} - --- '{x, y, z} -notation `'{`:max a:(foldr `, ` (x b, insert_same_level x b) ∅) `}`:0 := a - -theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a := -take y, assume ys, or.inr ys - -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 - -/- singleton -/ - -open trunc_index - -theorem mem_singleton_iff {X : Type} [is_set X] (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) - -theorem mem_singleton (a : X) : a ∈ '{a} := !mem_insert - -theorem eq_of_mem_singleton {X : Type} [is_set X] {x y : X} (h : x ∈ '{y}) : x = y := -or.elim (eq_or_mem_of_mem_insert h) - (suppose x = y, this) - (suppose x ∈ ∅, absurd this (not_mem_empty x)) - -theorem mem_singleton_of_eq {x y : X} (H : x = y) : x ∈ '{y} := -eq.symm H ▸ mem_singleton y - -/- -theorem insert_eq (x : X) (s : set X) : insert x s = '{x} ∪ s := -ext (take y, iff.intro - (suppose y ∈ insert x s, - or.elim this (suppose y = x, or.inl (or.inl this)) (suppose y ∈ s, or.inr this)) - (suppose y ∈ '{x} ∪ s, - or.elim this - (suppose y ∈ '{x}, or.inl (eq_of_mem_singleton this)) - (suppose y ∈ s, or.inr this))) --/ - -/- -theorem pair_eq_singleton (a : X) : '{a, a} = '{a} := -by rewrite [insert_eq_of_mem !mem_singleton] --/ -/- -theorem singleton_ne_empty (a : X) : '{a} ≠ ∅ := -begin - intro H, - apply not_mem_empty a, - rewrite -H, - apply mem_insert -end --/ - -end set