source
instance instDecidablePredComp_batteries {α : Sort u_1} {β : Sort u_2} {p : β → Prop} {f : α → β} [DecidablePred p] :
DecidablePred (p ∘ f)
Equations

- instDecidablePredComp_batteries = inferInstanceAs (DecidablePred fun (x : α) => p (f x))

## id #

source
theorem Function.id_def {α : Sort u_1} :
id = fun (x : α) => x

## decidable #

source
theorem Decidable.exists_not_of_not_forall {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] :
(¬∀ (x : α), p x) → ∃ (x : α), ¬p x

Alias of the forward direction of `Decidable.not_forall`.

## classical logic #

source
theorem Classical.exists_not_of_not_forall {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), p x) → ∃ (x : α), ¬p x

Alias of the forward direction of `Classical.not_forall`.

## equality #

source
theorem heq_iff_eq {α : Sort u_1} {a b : α} :
a ≍ b ↔ a = b
source
@[simp]
theorem eq_rec_constant {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a') :
h ▸ y = y
source
theorem congrArg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β} (hx : x = x') (hy : y = y') :
f x y = f x' y'
source
theorem congrFun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :
f a b = g a b
source
theorem congrFun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
f a b c = g a b c
source
theorem funext₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b} (h : ∀ (a : α) (b : β a), f a b = g a b) :
f = g
source
theorem funext₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c) :
f = g
source
theorem Eq.congr {α✝ : Sort u_1} {x₁ y₁ x₂ y₂ : α✝} (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) :
x₁ = x₂ ↔ y₁ = y₂
source
theorem Eq.congr_left {α : Sort u_1} {x y z : α} (h : x = y) :
x = z ↔ y = z
source
theorem Eq.congr_right {α : Sort u_1} {x y z : α} (h : x = y) :
z = x ↔ z = y
source
theorem congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) :
f a₁ = f a₂

Alias of `congrArg`.

source
theorem congr_arg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x x' : α} {y y' : β} (hx : x = x') (hy : y = y') :
f x y = f x' y'

Alias of `congrArg₂`.

source
theorem congr_fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) :
f a = g a

Alias of `congrFun`.

source
theorem congr_fun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :
f a b = g a b

Alias of `congrFun₂`.

source
theorem congr_fun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :
f a b c = g a b c

Alias of `congrFun₃`.

source
theorem heq_of_cast_eq {α β : Sort u_1} {a : α} {a' : β} (e : α = β) :
cast e a = a' → a ≍ a'
source
theorem cast_eq_iff_heq {a✝ a✝¹ : Sort u_1} {e : a✝ = a✝¹} {a : a✝} {a' : a✝¹} :
cast e a = a' ↔ a ≍ a'
source
theorem eqRec_eq_cast {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :
e ▸ x = cast ⋯ x
source
theorem eqRec_heq_self {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :
e ▸ x ≍ x
source
@[simp]
theorem eqRec_heq_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :
e ▸ x ≍ y ↔ x ≍ y
source
@[simp]
theorem heq_eqRec_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :
y ≍ e ▸ x ↔ y ≍ x

## miscellaneous #

source
@[simp]
theorem not_nonempty_empty :
¬Nonempty Empty
source
@[simp]
theorem not_nonempty_pempty :
¬Nonempty PEmpty
source
theorem subsingleton_of_forall_eq {α : Sort u_1} (x : α) (h : ∀ (y : α), y = x) :
Subsingleton α

If all points are equal to a given point `x`, then `α` is a subsingleton.

source
theorem subsingleton_iff_forall_eq {α : Sort u_1} (x : α) :
Subsingleton α ↔ ∀ (y : α), y = x
source
theorem congr_eqRec {α : Sort u_1} {γ : Sort u_2} {x x' : α} {β : α → Sort u_3} (f : (x : α) → β x → γ) (h : x = x') (y : β x) :
f x' (h ▸ y) = f x y