diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 93e7aaa..7888a68 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -38,6 +38,12 @@ lemma fix_antitone {X : Type} [PermSet 𝔸 X] {S T : Set X} : S ⊆ T → PermS intro hsub π hπ x hx exact hπ x (hsub hx) +/-- Restatement of `fix_antitone` that is sometimes more convenient for use with apply. -/ +lemma fix_antitone_mem {X : Type} [PermSet 𝔸 X] {S T : Set X} {π : FPerm 𝔸} : + π ∈ PermSet.fix 𝔸 T → S ⊆ T → π ∈ PermSet.fix 𝔸 S := by + intro hπ hsub + exact fix_antitone 𝔸 hsub hπ + /-- If π fixes S ∪ T, it fixes both S and T. -/ lemma fix_union {X : Type} [PermSet 𝔸 X] {S T : Set X} : PermSet.fix 𝔸 (S ∪ T) ⊆ PermSet.fix 𝔸 S ∩ PermSet.fix 𝔸 T := by apply Set.subset_inter <;> all_goals simp [fix_antitone] |