In this file we prove some basic properties about the typeclass IsEmpty.

@[simp]

theorem not_nonempty_iff {α : Sort u_1} : ¬Nonempty α ↔ IsEmpty α

@[simp]

theorem not_isEmpty_iff {α : Sort u_1} : ¬IsEmpty α ↔ Nonempty α

@[simp]

theorem isEmpty_Prop {p : Prop} : IsEmpty p ↔ ¬p

@[simp]

theorem isEmpty_pi {α : Sort u_1} {π : α → Sort u_4} : IsEmpty ((a : α) → π a) ↔ ∃ (a : α), IsEmpty (π a)

theorem isEmpty_fun {α : Sort u_1} {β : Sort u_2} : IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

@[simp]

theorem nonempty_fun {α : Sort u_1} {β : Sort u_2} : Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β

@[simp]

theorem isEmpty_sigma {α : Type u_5} {E : α → Type u_4} : IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)

@[simp]

theorem isEmpty_psigma {α : Sort u_5} {E : α → Sort u_4} : IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)

theorem isEmpty_subtype {α : Sort u_1} (p : α → Prop) : IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x

@[simp]

theorem isEmpty_prod {α : Type u_4} {β : Type u_5} : IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

@[simp]

theorem isEmpty_pprod {α : Sort u_1} {β : Sort u_2} : IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β

@[simp]

theorem isEmpty_sum {α : Type u_4} {β : Type u_5} : IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

@[simp]

theorem isEmpty_psum {α : Sort u_4} {β : Sort u_5} : IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

@[simp]

theorem isEmpty_ulift {α : Type u_4} : IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α

@[simp]

theorem isEmpty_plift {α : Sort u_4} : IsEmpty (PLift α) ↔ IsEmpty α

theorem wellFounded_of_isEmpty {α : Sort u_4} [IsEmpty α] (r : α → α → Prop) : WellFounded r

theorem isEmpty_or_nonempty (α : Sort u_1) : IsEmpty α ∨ Nonempty α

@[simp]

theorem not_isEmpty_of_nonempty (α : Sort u_1) [h : Nonempty α] : ¬IsEmpty α

theorem Function.extend_of_isEmpty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) : extend f g h = h

@[simp]

theorem leftTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.LeftTotal R

theorem leftTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.LeftTotal R ↔ IsEmpty α

@[simp]

theorem rightTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.RightTotal R

theorem rightTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.RightTotal R ↔ IsEmpty β

@[simp]

theorem biTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] [IsEmpty β] : Relator.BiTotal R

theorem biTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.BiTotal R ↔ IsEmpty β

theorem biTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.BiTotal R ↔ IsEmpty α

theorem Function.Surjective.of_isEmpty {α : Type u_4} {β : Type u_5} [IsEmpty β] (f : α → β) : Surjective f

theorem Function.surjective_iff_isEmpty {α : Type u_4} {β : Type u_5} [IsEmpty α] (f : α → β) : Surjective f ↔ IsEmpty β

theorem Function.Bijective.of_isEmpty {α : Type u_4} {β : Type u_5} (f : α → β) [IsEmpty β] : Bijective f

theorem Function.not_surjective_of_isEmpty_of_nonempty {α : Type u_4} {β : Type u_5} [IsEmpty α] [Nonempty β] (f : α → β) : ¬Surjective f