diff options
| -rw-r--r-- | Nominal/Helpers/Finset.lean | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Nominal/Helpers/Finset.lean b/Nominal/Helpers/Finset.lean new file mode 100644 index 0000000..1287c8e --- /dev/null +++ b/Nominal/Helpers/Finset.lean @@ -0,0 +1,23 @@ +import Mathlib.Tactic + +namespace Finset.Nonempty + +theorem induction + {α : Type} {motive : Finset α → Prop} [DecidableEq α] + (single : ∀ (a : α), motive {a}) + (insert : ∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) + : ∀ s, Finset.Nonempty s → motive s := by + intro S + induction' S using Finset.induction + · simp + · expose_names + intro _ + by_cases h : (Finset.Nonempty s) + · apply insert + · assumption + · apply h_1; assumption + · simp at h + rw [h] + apply single + +end Finset.Nonempty |