From 091fd832586627fbf31375fb5487d5e6fa6f7053 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 26 Oct 2025 13:26:57 +0100 Subject: finish name abstraction proofs --- Nominal/Equivariance.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Nominal/Equivariance.lean') 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`". -/ -- cgit v1.3.1