diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 64cc371..89021a0 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -170,6 +170,24 @@ lemma support_sInter {x : X} {C : Set (Set 𝔸)}: C.Finite → C.Nonempty → ( · exact support_inter 𝔸 hsing.left hsing.right hC'.left hC'.right · apply Set.Finite.inter_of_left hsing.right +/-- If two permutations π and σ are equal for all atoms in a support of x, then πx = σx. -/ +lemma support_permutations_eq {π σ : FPerm 𝔸} {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → (∀ a ∈ S, π a = σ a) → π • x = σ • x := by + intro hsupp heq + have hfix : σ⁻¹ * π ∈ PermSet.fix 𝔸 S := by + intro a ha + calc + (σ⁻¹ * π) • a = σ⁻¹ (π a) := rfl + _ = σ⁻¹ (σ a) := by rw [heq a ha] + _ = (σ⁻¹ * σ) a := rfl + _ = (1 : FPerm 𝔸) a := by rw [inv_mul_cancel] + _ = a := rfl + calc + π • x = (1 * π) • x := rfl + _ = (σ * σ⁻¹ * π) • x := by rw [mul_inv_cancel] + _ = (σ * (σ⁻¹ * π)) • x := rfl + _ = σ • ((σ⁻¹ * π) • x) := by rw [smul_smul] + _ = σ • x := by rw [hsupp hfix] + end PermSet end Support @@ -286,10 +304,20 @@ lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by obtain ⟨a, ⟨_, ha⟩⟩ := Set.Infinite.exists_notMem_finite h_inf h_fin use a +/-- If a and b are fresh for x, then (a b) fixes x. -/ +lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ PermSet.fix' 𝔸 x := by + intro ha hb + suffices ⸨a, b⸩ • x = (1 : FPerm 𝔸) • x by + simp only [one_smul, PermSet.fix', Set.mem_setOf_eq] at *; assumption + apply PermSet.support_permutations_eq + · exact supp_is_support 𝔸 + · intro c hc + apply FPerm.swap_neq (ne_of_mem_of_not_mem hc ha) (ne_of_mem_of_not_mem hc hb) + /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by simp [NominalSet.ForFresh]; intro h - exact Set.Infinite.nonempty h + exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a) = (И a, Q a) := by |