Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2021 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
! This file was ported from Lean 3 source module logic.is_empty
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Logic.Function.Basic
/-!
# Types that are empty
In this file we define a typeclass `IsEmpty`, which expresses that a type has no elements.
## Main declaration
* `IsEmpty`: a typeclass that expresses that a type is empty.
-/
variable { α β γ : Sort _ }
/-- `IsEmpty α` expresses that `α` is empty. -/
class IsEmpty ( α : Sort _ ) : Prop where
protected false : α → False
#align is_empty IsEmpty
instance : IsEmpty Empty :=
⟨ Empty.elim ⟩
instance : IsEmpty PEmpty :=
⟨ PEmpty.elim ⟩
instance : IsEmpty False :=
⟨ id : ∀ {α : Sort ?u.104}, α → α ⟩
instance Fin.isEmpty : IsEmpty ( Fin 0 ) :=
⟨ fun n ↦ Nat.not_lt_zero : ∀ (n : ℕ ), ¬ n < 0 n . 1 n . 2 : ∀ {n : ℕ } (self : Fin n ↑self < n ⟩
protected theorem Function.isEmpty [ IsEmpty β ] ( f : α → β ) : IsEmpty α :=
⟨ fun x ↦ IsEmpty.false ( f x )⟩
#align function.is_empty Function.isEmpty
instance { p : α → Sort _ } [ h : Nonempty α ] [∀ x , IsEmpty ( p x )] : IsEmpty (∀ x , p x ) :=
h . elim fun x ↦ Function.isEmpty <| Function.eval : {α : Sort ?u.259} → {β : α → Sort ?u.258(x : α ) → ((x : α ) → β x ) → β x x
instance PProd.isEmpty_left [ IsEmpty α ] : IsEmpty ( PProd : Sort ?u.322 → Sort ?u.321 → Sort (max(max1?u.322)?u.321) α β ) :=
Function.isEmpty PProd.fst
instance PProd.isEmpty_right [ IsEmpty β ] : IsEmpty ( PProd : Sort ?u.383 → Sort ?u.382 → Sort (max(max1?u.383)?u.382) α β ) :=
Function.isEmpty PProd.snd
instance Prod.isEmpty_left { α β } [ IsEmpty α ] : IsEmpty ( α × β ) :=
Function.isEmpty Prod.fst : {α : Type ?u.473} → {β : Type ?u.472} → α × β α
instance Prod.isEmpty_right { α β } [ IsEmpty β ] : IsEmpty ( α × β ) :=
Function.isEmpty Prod.snd : {α : Type ?u.547} → {β : Type ?u.546} → α × β β
instance [ IsEmpty α ] [ IsEmpty β ] : IsEmpty ( PSum : Sort ?u.595 → Sort ?u.594 → Sort (max(max1?u.595)?u.594) α β ) :=
⟨ fun x ↦ PSum.rec : ∀ {α : Sort ?u.608} {β : Sort ?u.607} {motive : α ⊕' β Sort ?u.609(∀ (val : α ), motive (PSum.inl val ) → (∀ (val : β ), motive (PSum.inr val ) → ∀ (t : α ⊕' β motive t IsEmpty.false IsEmpty.false x ⟩
instance { α β } [ IsEmpty α ] [ IsEmpty β ] : IsEmpty ( Sum α β ) :=
⟨ fun x ↦ Sum.rec : ∀ {α : Type ?u.759} {β : Type ?u.758} {motive : α ⊕ β Sort ?u.760(∀ (val : α ), motive (Sum.inl val ) → (∀ (val : β ), motive (Sum.inr val ) → ∀ (t : α ⊕ β motive t IsEmpty.false IsEmpty.false x ⟩
/-- subtypes of an empty type are empty -/
instance [ IsEmpty α ] ( p : α → Prop ) : IsEmpty ( Subtype p ) :=
⟨ fun x ↦ IsEmpty.false x . 1 ⟩
/-- subtypes by an all-false predicate are false. -/
theorem Subtype.isEmpty_of_false { p : α → Prop } ( hp : ∀ a , ¬ p a ) : IsEmpty ( Subtype p ) :=
⟨ fun x ↦ hp _ x . 2 ⟩
#align subtype.is_empty_of_false Subtype.isEmpty_of_false
/-- subtypes by false are false. -/
instance Subtype.isEmpty_false : IsEmpty { _a : α // False } :=
Subtype.isEmpty_of_false fun _ ↦ id : ∀ {α : Sort ?u.1049}, α → α
instance Sigma.isEmpty_left { α } [ IsEmpty α ] { E : α → Type _ } : IsEmpty ( Sigma : {α : Type ?u.1090} → (α → Type ?u.1089Type (max?u.1090?u.1089) E ) :=
Function.isEmpty Sigma.fst : {α : Type ?u.1125} → {β : α → Type ?u.1124Sigma β α
example [ h : Nonempty α ] [ IsEmpty β ] : IsEmpty ( α → β ) := by infer_instance
/-- Eliminate out of a type that `IsEmpty` (without using projection notation). -/
@[elab_as_elim]
def isEmptyElim : {α : Sort u_1} → [inst : IsEmpty α {p : α → Sort u_2(a : α ) → p a isEmptyElim [ IsEmpty α ] { p : α → Sort _ } ( a : α ) : p a :=
( IsEmpty.false a ). elim
#align is_empty_elim isEmptyElim : {α : Sort u_1} → [inst : IsEmpty α {p : α → Sort u_2(a : α ) → p a
theorem isEmpty_iff : IsEmpty α ↔ α → False :=
⟨@ IsEmpty.false α , IsEmpty.mk ⟩
#align is_empty_iff isEmpty_iff
namespace IsEmpty
open Function
/-- Eliminate out of a type that `IsEmpty` (using projection notation). -/
@[elab_as_elim]
protected def elim { α : Sort u } ( _ : IsEmpty α ) { p : α → Sort _ } ( a : α ) : p a :=
isEmptyElim : {α : Sort ?u.1396} → [inst : IsEmpty α {p : α → Sort ?u.1395(a : α ) → p a a
#align is_empty.elim IsEmpty.elim : {α : Sort u} → IsEmpty α {p : α → Sort u_1(a : α ) → p a
/-- Non-dependent version of `IsEmpty.elim`. Helpful if the elaborator cannot elaborate `h.elim a`
correctly. -/
protected def elim' { β : Sort _ } ( h : IsEmpty α ) ( a : α ) : β :=
( h . false a ). elim
#align is_empty.elim' IsEmpty.elim'
protected theorem prop_iff { p : Prop } : IsEmpty p ↔ ¬ p :=
isEmpty_iff
#align is_empty.prop_iff IsEmpty.prop_iff
variable [ IsEmpty α ]
@[ simp ]
theorem forall_iff { p : α → Prop } : (∀ a , p a ) ↔ True :=
iff_true_intro isEmptyElim : ∀ {α : Sort ?u.1649} [inst : IsEmpty α p : α → Sort ?u.1648a : α ), p a
#align is_empty.forall_iff IsEmpty.forall_iff
@[ simp ]
theorem exists_iff { p : α → Prop } : (∃ a , p a ) ↔ False :=
iff_false_intro fun ⟨ x , _⟩ ↦ IsEmpty.false x
#align is_empty.exists_iff IsEmpty.exists_iff
-- see Note [lower instance priority]
instance ( priority := 100) : Subsingleton α :=
⟨ isEmptyElim : ∀ {α : Sort ?u.1920} [inst : IsEmpty α p : α → Sort ?u.1919a : α ), p a ⟩
end IsEmpty
@[ simp ]
theorem not_nonempty_iff : ¬ Nonempty α ↔ IsEmpty α :=
⟨ fun h ↦ ⟨ fun x ↦ h ⟨ x ⟩⟩, fun h1 h2 ↦ h2 . elim h1 . elim : ∀ {α : Sort ?u.2042}, IsEmpty α ∀ {p : α → Sort ?u.2041a : α ), p a ⟩
#align not_nonempty_iff not_nonempty_iff
@[ simp ]
theorem not_isEmpty_iff : ¬ IsEmpty α ↔ Nonempty α :=
not_iff_comm : ∀ {a b : Prop }, (¬ a ↔ b ↔ (¬ b ↔ a . mp : ∀ {a b : Prop }, (a ↔ b a → b not_nonempty_iff
#align not_is_empty_iff not_isEmpty_iff
@[ simp ]
theorem isEmpty_Prop { p : Prop } : IsEmpty p ↔ ¬ p := by
simp only [← not_nonempty_iff , nonempty_Prop ]
#align is_empty_Prop isEmpty_Prop
@[ simp ]
theorem isEmpty_pi { π : α → Sort _ } : IsEmpty (∀ a , π a ) ↔ ∃ a , IsEmpty ( π a ) := by
simp only [← not_nonempty_iff , Classical.nonempty_pi , not_forall : ∀ {α : Sort ?u.2265} {p : α → Prop (¬ ∀ (x : α ), p x ↔ ∃ x , ¬ p x ]
#align is_empty_pi isEmpty_pi
@[ simp ]
theorem isEmpty_sigma { α } { E : α → Type _ } : IsEmpty ( Sigma : {α : Type ?u.2441} → (α → Type ?u.2440Type (max?u.2441?u.2440) E ) ↔ ∀ a , IsEmpty ( E a ) := by
simp only [← not_nonempty_iff , nonempty_sigma , not_exists : ∀ {α : Sort ?u.2491} {p : α → Prop (¬ ∃ x , p x ↔ ∀ (x : α ), ¬ p x ]
#align is_empty_sigma isEmpty_sigma
@[ simp ]
theorem isEmpty_psigma { α } { E : α → Sort _ } : IsEmpty ( PSigma : {α : Sort ?u.2660} → (α → Sort ?u.2659Sort (max(max1?u.2660)?u.2659) E ) ↔ ∀ a , IsEmpty ( E a ) := by
simp only [← not_nonempty_iff , nonempty_psigma , not_exists : ∀ {α : Sort ?u.2710} {p : α → Prop (¬ ∃ x , p x ↔ ∀ (x : α ), ¬ p x ]
#align is_empty_psigma isEmpty_psigma
@[ simp ]
theorem isEmpty_subtype ( p : α → Prop ) : IsEmpty ( Subtype : {α : Sort ?u.2863} → (α → Prop Sort (max1?u.2863) p ) ↔ ∀ x , ¬ p x := by
simp only [← not_nonempty_iff , nonempty_subtype , not_exists : ∀ {α : Sort ?u.2910} {p : α → Prop (¬ ∃ x , p x ↔ ∀ (x : α ), ¬ p x ]
#align is_empty_subtype isEmpty_subtype
@[ simp ]
theorem isEmpty_prod { α β : Type _ } : IsEmpty ( α × β ) ↔ IsEmpty α ∨ IsEmpty β := by
simp only [← not_nonempty_iff , nonempty_prod , not_and_or ]
#align is_empty_prod isEmpty_prod
@[ simp ]
theorem isEmpty_pprod : IsEmpty ( PProd : Sort ?u.3181 → Sort ?u.3180 → Sort (max(max1?u.3181)?u.3180) α β ) ↔ IsEmpty α ∨ IsEmpty β := by
simp only [← not_nonempty_iff , nonempty_pprod , not_and_or ]
#align is_empty_pprod isEmpty_pprod
@[ simp ]
theorem isEmpty_sum { α β } : IsEmpty ( Sum α β ) ↔ IsEmpty α ∧ IsEmpty β := by
simp only [← not_nonempty_iff , nonempty_sum , not_or ]
#align is_empty_sum isEmpty_sum
@[ simp ]
theorem isEmpty_psum { α β } : IsEmpty ( PSum : Sort ?u.3473 → Sort ?u.3472 → Sort (max(max1?u.3473)?u.3472) α β ) ↔ IsEmpty α ∧ IsEmpty β := by
simp only [← not_nonempty_iff , nonempty_psum , not_or ]
#align is_empty_psum isEmpty_psum
@[ simp ]
theorem isEmpty_ulift { α } : IsEmpty ( ULift : Type ?u.3614 → Type (max?u.3614?u.3615) α ) ↔ IsEmpty α := by
simp only [← not_nonempty_iff , nonempty_ulift ]
#align is_empty_ulift isEmpty_ulift
@[ simp ]
theorem isEmpty_plift { α } : IsEmpty ( PLift α ) ↔ IsEmpty α := by
simp only [← not_nonempty_iff , nonempty_plift ]
#align is_empty_plift isEmpty_plift
theorem wellFounded_of_isEmpty { α } [ IsEmpty α ] ( r : α → α → Prop ) : WellFounded r :=
⟨ isEmptyElim : ∀ {α : Sort ?u.3840} [inst : IsEmpty α p : α → Sort ?u.3839a : α ), p a ⟩
#align well_founded_of_empty wellFounded_of_isEmpty
variable ( α )
theorem isEmpty_or_nonempty : IsEmpty α ∨ Nonempty α :=
( em <| IsEmpty α ). elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c elim Or.inl : ∀ {a b : Prop }, a → a ∨ b <| Or.inr : ∀ {a b : Prop }, b → a ∨ b ∘ not_isEmpty_iff . mp : ∀ {a b : Prop }, (a ↔ b a → b
#align is_empty_or_nonempty isEmpty_or_nonempty
@[ simp ]
theorem not_isEmpty_of_nonempty [ h : Nonempty α ] : ¬ IsEmpty α :=
not_isEmpty_iff . mpr : ∀ {a b : Prop }, (a ↔ b b → a h
#align not_is_empty_of_nonempty not_isEmpty_of_nonempty
variable { α }
theorem Function.extend_of_isEmpty : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [inst : IsEmpty α f : α → β g : α → γ h : β → γ extend f g h = h Function.extend_of_isEmpty [ IsEmpty α ] ( f : α → β ) ( g : α → γ ) ( h : β → γ ) :
Function.extend : {α : Sort ?u.4052} → {β : Sort ?u.4051} → {γ : Sort ?u.4050} → (α → β (α → γ (β → γ β → γ f g h = h :=
funext : ∀ {α : Sort ?u.4075} {β : α → Sort ?u.4074f g : (x : α ) → β x }, (∀ (x : α ), f x = g x ) → f = g fun _ ↦ ( Function.extend_apply' : ∀ {α : Sort ?u.4091} {β : Sort ?u.4092} {γ : Sort ?u.4093} {f : α → β g : α → γ e' : β → γ b : β ),
(¬ ∃ a , f a = b extend f g e' b = e' b _ _ _ ) fun ⟨ a , _⟩ ↦ isEmptyElim : ∀ {α : Sort ?u.4154} [inst : IsEmpty α p : α → Sort ?u.4153a : α ), p a a
#align function.extend_of_empty Function.extend_of_isEmpty