diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index b8e6809..93e7aaa 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -153,9 +153,9 @@ lemma support_inter {x : X} {S T : Set ๐ธ} : HasSupport ๐ธ x S โ S.Finite /-- For a finite number of finite supports, the intersection is also a support. -/ lemma support_sInter {x : X} {C : Set (Set ๐ธ)}: C.Finite โ C.Nonempty โ (โ S โ C, HasSupport ๐ธ x S โง S.Finite) โ HasSupport ๐ธ x (โโ C) := by - suffices (C : Finset (Set ๐ธ)) : C.Nonempty โ (โ S โ C, HasSupport ๐ธ x S โง S.Finite) โ HasSupport ๐ธ x (โโ C.toSet) โง (โโ C.toSet).Finite + suffices (C : Finset (Set ๐ธ)) : C.Nonempty โ (โ S โ C, HasSupport ๐ธ x S โง S.Finite) โ HasSupport ๐ธ x (โโ C) โง (โโ (โC : Set (Set ๐ธ))).Finite ยท intro hfin - rw [show C = hfin.toFinset.toSet by simp] + rw [show C = hfin.toFinset by simp] intro hne h exact (this hfin.toFinset hne h).left ยท have : DecidableEq (Set ๐ธ) := Classical.typeDecidableEq (Set ๐ธ) |