michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/set/basic): add spaces in notation for bounded quantifiers

Browse source
This commit is contained in:
Jeremy Avigad 2016-03-03 11:50:40 -05:00
parent dc6cd71236
commit 87252bbffe
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/data/set/basic.lean
View file

@ -53,18 +53,18 @@ assume h, absurd rfl (and.elim_right h)
/- bounded quantification -/
abbreviation bounded_forall (a : set X) (P : X → Prop) := ∀⦃x⦄, x ∈ a → P x
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
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
abbreviation bounded_exists (a : set X) (P : X → Prop) := ∃⦃x⦄, x ∈ a ∧ P x
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
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
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)
lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x ∈ S, P x ↔ Q x) :
(∀₀ x ∈ S, P x) = (∀₀ x ∈ S, Q x) :=
begin
apply propext,
@ -74,7 +74,7 @@ begin
apply H
end
lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x ∈ S, P x ↔ Q x) :
(∃₀ x ∈ S, P x) = (∃₀ x ∈ S, Q x) :=
begin
apply propext,