Documentation

Mathlib.Basic.IsEmpty.Basic

Basic properties of IsEmpty #

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

source
@[simp]
theorem not_nonempty_iff {α : Sort u_1} :
¬Nonempty α ↔ IsEmpty α
source
@[simp]
theorem not_isEmpty_iff {α : Sort u_1} :
¬IsEmpty α ↔ Nonempty α
source
@[simp]
theorem isEmpty_Prop {p : Prop} :
IsEmpty p ↔ ¬p
source
@[simp]
theorem isEmpty_pi {α : Sort u_1} {π : α → Sort u_4} :
IsEmpty ((a : α) → π a) ↔ ∃ (a : α), IsEmpty (π a)
source
theorem isEmpty_fun {α : Sort u_1} {β : Sort u_2} :
IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
source
@[simp]
theorem nonempty_fun {α : Sort u_1} {β : Sort u_2} :
Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β
source
@[simp]
theorem isEmpty_sigma {α : Type u_5} {E : α → Type u_4} :
IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
source
@[simp]
theorem isEmpty_psigma {α : Sort u_5} {E : α → Sort u_4} :
IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
source
theorem isEmpty_subtype {α : Sort u_1} (p : α → Prop) :
IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
source
@[simp]
theorem isEmpty_prod {α : Type u_4} {β : Type u_5} :
IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
source
@[simp]
theorem isEmpty_pprod {α : Sort u_1} {β : Sort u_2} :
IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β
source
@[simp]
theorem isEmpty_sum {α : Type u_4} {β : Type u_5} :
IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
source
@[simp]
theorem isEmpty_psum {α : Sort u_4} {β : Sort u_5} :
IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
source
@[simp]
theorem isEmpty_ulift {α : Type u_4} :
IsEmpty (ULift α) ↔ IsEmpty α
source
@[simp]
theorem isEmpty_plift {α : Sort u_4} :
IsEmpty (PLift α) ↔ IsEmpty α
source
theorem wellFounded_of_isEmpty {α : Sort u_4} [IsEmpty α] (r : α → α → Prop) :
WellFounded r
source
theorem isEmpty_or_nonempty (α : Sort u_1) :
IsEmpty α ∨ Nonempty α
source
@[simp]
theorem not_isEmpty_of_nonempty (α : Sort u_1) [h : Nonempty α] :
¬IsEmpty α
source
theorem Function.extend_of_isEmpty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) :
extend f g h = h
source
@[simp]
theorem leftTotal_empty {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty α] :
Relator.LeftTotal R
source
theorem leftTotal_iff_isEmpty_left {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty β] :
Relator.LeftTotal R ↔ IsEmpty α
source
@[simp]
theorem rightTotal_empty {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty β] :
Relator.RightTotal R
source
theorem rightTotal_iff_isEmpty_right {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty α] :
Relator.RightTotal R ↔ IsEmpty β
source
@[simp]
theorem biTotal_empty {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty α] [IsEmpty β] :
Relator.BiTotal R
source
theorem biTotal_iff_isEmpty_right {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty α] :
Relator.BiTotal R ↔ IsEmpty β
source
theorem biTotal_iff_isEmpty_left {α : Sort u_1} {β : Sort u_2} (R : α → β → Prop) [IsEmpty β] :
Relator.BiTotal R ↔ IsEmpty α
source
theorem Function.Surjective.of_isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty β] (f : α → β) :
Surjective f
source
theorem Function.surjective_iff_isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] (f : α → β) :
Surjective f ↔ IsEmpty β
source
theorem Function.Bijective.of_isEmpty {α : Sort u_1} {β : Sort u_2} (f : α → β) [IsEmpty β] :
Bijective f
source
theorem Function.not_surjective_of_isEmpty_of_nonempty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] [Nonempty β] (f : α → β) :
¬Surjective f