diff options
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`". -/ |