diff options
Diffstat (limited to 'Nominal/Equivariance.lean')
| -rw-r--r-- | Nominal/Equivariance.lean | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index ac50519..8475a21 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -185,6 +185,27 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸 end Nominal /-! +## Freshness + +For propositions of the form `И a, a R x`, where `R` is an equivariant relation, we do not have to differentiate between "for any fresh a" and "for all fresh a". +-/ +section Freshness + +namespace Equivariance + +variable {X : Type} [NominalSet 𝔸 X] {R: Rel 𝔸 X} {x : X} + +/-- The quantifier in `И a, a R x` is equivalent to "for any fresh `a`". -/ +lemma for_fresh_iff_exists : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∃ a, a # x ∧ R a x)) := by sorry + +/-- The quantifier in `И a, a R x` is equivalent to "for all fresh `a`". -/ +lemma for_fresh_iff_all : EquivariantRelation 𝔸 R → ((И a, R a x) ↔ (∀ a, a # x → R a x)) := by sorry + +end Equivariance + +end Freshness + +/-! ## Bundled Functions In the following, we also define a bundled function type for equivariant functions. |