From 8dddad262dc30b307583f458115955e37d6ed657 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 24 Mar 2024 17:50:33 +0000 Subject: [PATCH] feat(Logic/IsEmpty): add instances for `Quot` and `Quotient` (#11616) --- Mathlib/Logic/IsEmpty.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Logic/IsEmpty.lean b/Mathlib/Logic/IsEmpty.lean index 9b10e299d2ccdb..888b756009296c 100644 --- a/Mathlib/Logic/IsEmpty.lean +++ b/Mathlib/Logic/IsEmpty.lean @@ -46,6 +46,9 @@ protected theorem Function.isEmpty [IsEmpty β] (f : α → β) : IsEmpty α := ⟨fun x ↦ IsEmpty.false (f x)⟩ #align function.is_empty Function.isEmpty +theorem Function.Surjective.isEmpty [IsEmpty α] {f : α → β} (hf : f.Surjective) : IsEmpty β := + ⟨fun y ↦ let ⟨x, _⟩ := hf y; IsEmpty.false x⟩ + instance {p : α → Sort*} [h : Nonempty α] [∀ x, IsEmpty (p x)] : IsEmpty (∀ x, p x) := h.elim fun x ↦ Function.isEmpty <| Function.eval x @@ -61,6 +64,12 @@ instance Prod.isEmpty_left {α β} [IsEmpty α] : IsEmpty (α × β) := instance Prod.isEmpty_right {α β} [IsEmpty β] : IsEmpty (α × β) := Function.isEmpty Prod.snd +instance Quot.instIsEmpty {α : Sort*} [IsEmpty α] {r : α → α → Prop} : IsEmpty (Quot r) := + Function.Surjective.isEmpty Quot.exists_rep + +instance Quotient.instIsEmpty {α : Sort*} [IsEmpty α] {s : Setoid α} : IsEmpty (Quotient s) := + Quot.instIsEmpty + instance [IsEmpty α] [IsEmpty β] : IsEmpty (PSum α β) := ⟨fun x ↦ PSum.rec IsEmpty.false IsEmpty.false x⟩