diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 13:26:57 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-26 13:31:36 +0100 |
| commit | 091fd832586627fbf31375fb5487d5e6fa6f7053 (patch) | |
| tree | aac1679d86d15e2b9c89c2bd5efb7fd8b97980a0 /Nominal/Equivariance.lean | |
| parent | 10edba2c0365a6858a74da22042c98f9d5fa1acc (diff) | |
finish name abstraction proofs
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 57c6d11..189ca66 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -215,6 +215,8 @@ variable {X : Type} [NominalSet 𔸠X] {R: Rel 𔸠X} {x : X} private lemma for_fresh_iffâ‚ : EquivariantRelation 𔸠R → (И a, R a x) → (∃ a, a # x ∧ R a x) := by intro hequi h + apply Set.Finite.infinite_compl at h + simp at h have hinf : ({a | R a x} \ NominalSet.supp 𔸠x).Infinite := Set.Infinite.diff h (NominalSet.supp_finite ð”¸) obtain ⟨a, ha⟩ := hinf.nonempty simp only [Set.mem_diff, Set.mem_setOf_eq] at ha @@ -237,7 +239,6 @@ private lemma for_fresh_iff₃ : EquivariantRelation 𔸠R → (∀ a, a # x ↠rw [Set.mem_compl_iff] at ha exact h a ha simp only [NominalSet.ForFresh] - apply Set.infinite_of_finite_compl apply Set.Finite.subset (NominalSet.supp_finite ð”¸) hsub /-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/ |