diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-11-30 22:20:35 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-11-30 22:33:32 +0100 |
| commit | e02ad2dcc0f93107c18f8316b386b92b45548e97 (patch) | |
| tree | e1c341a5fe9be21a2d2ed9086dd19f3d29fee8f0 /Nominal/Support.lean | |
| parent | ea38ef0cb2c57e10696c7fb6108732a6f454818c (diff) | |
update lean
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 ๐ธ) |