From e02ad2dcc0f93107c18f8316b386b92b45548e97 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 30 Nov 2025 22:20:35 +0100 Subject: update lean --- Nominal/Support.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Nominal/Support.lean') 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 ๐”ธ) -- cgit v1.3.1