feat(data/finite/defs): add ulift.infinite/plift.infinite (#17655)

leanprover-community · Nov 22, 2022 · f69e8f3 · f69e8f3
1 parent cadea04
commit f69e8f3
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/data/finite/defs.lean b/src/data/finite/defs.lean
@@ -83,6 +83,12 @@ class infinite (α : Sort*) : Prop :=
 @[simp] lemma not_infinite_iff_finite : ¬infinite α ↔ finite α :=
 not_finite_iff_infinite.not_right.symm
 
+lemma equiv.infinite_iff (e : α ≃ β) : infinite α ↔ infinite β :=
+not_finite_iff_infinite.symm.trans $ e.finite_iff.not.trans not_finite_iff_infinite
+
+instance [infinite α] : infinite (plift α) := equiv.plift.infinite_iff.2 ‹_›
+instance {α : Type v} [infinite α] : infinite (ulift.{u} α) := equiv.ulift.infinite_iff.2 ‹_›
+
 lemma finite_or_infinite (α : Sort*) : finite α ∨ infinite α :=
 or_iff_not_imp_left.2 $ not_finite_iff_infinite.1