From a06b288deb548cb5df919f4555b295305b70c910 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Aug 2015 18:47:20 -0700 Subject: [PATCH] fix(library/data/set/finite): the powerset notation has already been fixed --- library/data/set/finite.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/library/data/set/finite.lean b/library/data/set/finite.lean index f945e53e49..0a080695f8 100644 --- a/library/data/set/finite.lean +++ b/library/data/set/finite.lean @@ -129,11 +129,8 @@ by rewrite [-finset.to_set_upto n]; apply finite_finset theorem to_finset_upto (n : ℕ) : to_finset {i | i < n} = finset.upto n := by apply (to_finset_eq_of_to_set_eq !finset.to_set_upto) --- question: how can I avoid the parenthesis in the notation below? --- this didn't work: notation `𝒫`:max s := powerset s, nor variants - -theorem finite_powerset (s : set A) [fins : finite s] : finite (𝒫 s) := -assert H : (𝒫 s) = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))], +theorem finite_powerset (s : set A) [fins : finite s] : finite 𝒫 s := +assert H : 𝒫 s = finset.to_set '[finset.to_set (#finset 𝒫 (to_finset s))], from ext (take t, iff.intro (suppose t ∈ 𝒫 s, assert t ⊆ s, from this,