diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-12-03 20:34:41 +0100 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-12-03 20:34:41 +0100 |
| commit | 71a6a3d5b6f4b428b463bc4a0766c91d8c1d5768 (patch) | |
| tree | add4bf6d650df4b8ec743de45fc37dc7de16baaa /Nominal/Support.lean | |
| parent | 4ba4f11725d42286a2e94ee78dd938636ad2528a (diff) | |
refactor equivariant props to use type classes
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] |