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

Equations

• instDecidablePredCompProp = inferInstanceAs (DecidablePred fun (x : α) => p (f x))

@[deprecated proof_irrel]

theorem proofIrrel {a : Prop} (h₁ : a) (h₂ : a) : h₁ = h₂

Alias of proof_irrel.

exists and forall

theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} : (∀ (x : α), ¬p x) → ¬∃ (x : α), p x

Alias of the reverse direction of not_exists.

theorem forall_not_of_not_exists {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), p x) → ∀ (x : α), ¬p x

Alias of the forward direction of not_exists.

decidable

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

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

theorem heq_iff_eq : ∀ {α : Sort u_1} {a b : α}, HEq a b ↔ a = b

theorem proof_irrel_heq {p : Prop} {q : Prop} (hp : p) (hq : q) : HEq hp hq

@[simp]

theorem eq_rec_constant {α : Sort u_1} {a : α} {a' : α} {β : Sort u_2} (y : β) (h : a = a') : h ▸ y = y

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'

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

theorem congrFun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {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

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

theorem funext₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {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

theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : α → β) {x : α} {y : α} : f x ≠ f y → x ≠ y

theorem Eq.congr : ∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)

theorem Eq.congr_left {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) : x = z ↔ y = z

theorem Eq.congr_right {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) : z = x ↔ z = y

theorem congr_arg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

Alias of congrArg.

---

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

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₂.

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

Alias of congrFun.

---

Congruence in the function part of an application: If f = g then f a = g a.

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

Alias of congrFun₂.

theorem congr_fun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {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₃.

theorem eq_mp_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : Eq.mp h = cast h

theorem eq_mpr_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : Eq.mpr h = cast ⋯

@[simp]

theorem cast_cast {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) : cast hb (cast ha a) = cast ⋯ a

theorem heq_of_cast_eq {α : Sort u_1} {β : Sort u_1} {a : α} {a' : β} (e : α = β) : cast e a = a' → HEq a a'

theorem cast_eq_iff_heq : ∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ HEq a_2 a'

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

theorem eqRec_heq_self {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') : HEq (e ▸ x) x

@[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 : β) : HEq (e ▸ x) y ↔ HEq x y

@[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 : β) : HEq y (e ▸ x) ↔ HEq y x

membership

theorem ne_of_mem_of_not_mem {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {a : α} {b : α} (h : a ∈ s) : ¬b ∈ s → a ≠ b

theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {t : β} {a : α} (h : a ∈ s) : ¬a ∈ t → s ≠ t

miscellaneous

@[simp]

theorem not_nonempty_empty : ¬Nonempty Empty

@[simp]

theorem not_nonempty_pempty : ¬Nonempty PEmpty

theorem eq_iff_true_of_subsingleton {α : Sort u_1} [Subsingleton α] (x : α) (y : α) : x = y ↔ True

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.

theorem subsingleton_iff_forall_eq {α : Sort u_1} (x : α) : Subsingleton α ↔ ∀ (y : α), y = x

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