logic.basic

# Basic logic properties #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file is one of the earliest imports in mathlib.

## Implementation notes #

Theorems that require decidability hypotheses are in the namespace "decidable". Classical versions are in the namespace "classical".

In the presence of automation, this whole file may be unnecessary. On the other hand, maybe it is useful for writing automation.

@[reducible]
def hidden {α : Sort u_1} {a : α} :
α

An identity function with its main argument implicit. This will be printed as `hidden` even if it is applied to a large term, so it can be used for elision, as done in the `elide` and `unelide` tactics.

Equations
def empty.elim {C : Sort u_1} :

Ex falso, the nondependent eliminator for the `empty` type.

@[protected, instance]
@[protected, instance]
def subsingleton.prod {α : Type u_1} {β : Type u_2} [subsingleton α] [subsingleton β] :
@[protected, instance]
Equations
@[protected, instance]
def sort.inhabited  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def psum.inhabited_left {α : Sort u_1} {β : Sort u_2} [inhabited α] :
inhabited (psum α β)
Equations
@[protected, instance]
def psum.inhabited_right {α : Sort u_1} {β : Sort u_2} [inhabited β] :
inhabited (psum α β)
Equations
@[protected, instance]
Equations
@[simp]
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) :

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

theorem subsingleton_iff_forall_eq {α : Sort u_1} (x : α) :
(y : α), y = x
@[protected, instance]
def subtype.subsingleton (α : Sort u_1) [subsingleton α] (p : α Prop) :
@[simp]
theorem coe_coe {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [ β] [ γ] (a : α) :

Add an instance to "undo" coercion transitivity into a chain of coercions, because most simp lemmas are stated with respect to simple coercions and will not match when part of a chain.

theorem coe_fn_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : out_param Sort u_4)} [ β] [ γ] [ δ] (x : α) :
theorem coe_fn_coe_trans' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} [ β] [ γ] [ (λ (_x : γ), δ)] (x : α) :

Non-dependent version of `coe_fn_coe_trans`, helps `rw` figure out the argument.

@[simp]
theorem coe_fn_coe_base {α : Sort u_1} {β : Sort u_2} {γ : out_param Sort u_3)} [ β] [ γ] (x : α) :
theorem coe_fn_coe_base' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [ β] [ (λ (_x : β), γ)] (x : α) :

Non-dependent version of `coe_fn_coe_base`, helps `rw` figure out the argument.

theorem coe_sort_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : out_param (Sort u_4)} [ β] [ γ] [ δ] (x : α) :

Many structures such as bundled morphisms coerce to functions so that you can transparently apply them to arguments. For example, if `e : α ≃ β` and `a : α` then you can write `e a` and this is elaborated as `⇑e a`. This type of coercion is implemented using the `has_coe_to_fun` type class. There is one important consideration:

If a type coerces to another type which in turn coerces to a function, then it must implement `has_coe_to_fun` directly:

``````structure sparkling_equiv (α β) extends α ≃ β

-- if we add a `has_coe` instance,
instance {α β} : has_coe (sparkling_equiv α β) (α ≃ β) :=
⟨sparkling_equiv.to_equiv⟩

-- then a `has_coe_to_fun` instance **must** be added as well:
instance {α β} : has_coe_to_fun (sparkling_equiv α β) :=
⟨λ _, α → β, λ f, f.to_equiv.to_fun⟩
``````

(Rationale: if we do not declare the direct coercion, then `⇑e a` is not in simp-normal form. The lemma `coe_fn_coe_base` will unfold it to `⇑↑e a`. This often causes loops in the simplifier.)

@[simp]
theorem coe_sort_coe_base {α : Sort u_1} {β : Sort u_2} {γ : out_param (Sort u_3)} [ β] [ γ] (x : α) :
@[nolint]
inductive pempty  :

`pempty` is the universe-polymorphic analogue of `empty`.

Instances for `pempty`
@[protected, instance]
def pempty.elim {C : Sort u_1} :

Ex falso, the nondependent eliminator for the `pempty` type.

@[protected, instance]
@[simp]
theorem not_nonempty_pempty  :
theorem congr_heq {α β : Sort u_1} {γ : Sort u_2} {f : α γ} {g : β γ} {x : α} {y : β} (h₁ : f == g) (h₂ : x == y) :
f x = g y
theorem congr_arg_heq {α : Sort u_1} {β : α Sort u_2} (f : Π (a : α), β a) {a₁ a₂ : α} :
a₁ = a₂ f a₁ == f a₂
theorem ulift.down_injective {α : Type u_1} :
@[simp]
theorem ulift.down_inj {α : Type u_1} {a b : ulift α} :
a.down = b.down a = b
theorem plift.down_injective {α : Sort u_1} :
@[simp]
theorem plift.down_inj {α : Sort u_1} {a b : plift α} :
a.down = b.down a = b
theorem ne_comm {α : Sort u_1} {a b : α} :
a b b a
@[simp]
theorem eq_iff_eq_cancel_left {α : Sort u_1} {b c : α} :
( {a : α}, a = b a = c) b = c
@[simp]
theorem eq_iff_eq_cancel_right {α : Sort u_1} {a b : α} :
( {c : α}, a = c b = c) a = b
@[class]
structure fact (p : Prop) :
Prop
• out : p

Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details.

Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances.

For example, `zmod p` is a field if and only if `p` is a prime number. In order to be able to find this field instance automatically by type class search, we have to turn `p.prime` into an instance implicit assumption.

On the other hand, making `nat.prime` a class would require a major refactoring of the library, and it is questionable whether making `nat.prime` a class is desirable at all. The compromise is to add the assumption `[fact p.prime]` to `zmod.field`.

In particular, this class is not intended for turning the type class system into an automated theorem prover for first order logic.

Instances of this typeclass

In most cases, we should not have global instances of `fact`; typeclass search only reads the head symbol and then tries any instances, which means that adding any such instance will cause slowdowns everywhere. We instead make them as lemmata and make them local instances as required.

theorem fact.elim {p : Prop} (h : fact p) :
p
theorem fact_iff {p : Prop} :
fact p p
@[reducible]
def function.swap₂ {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁ Sort u_3} {κ₂ : ι₂ Sort u_4} {φ : Π (i₁ : ι₁), κ₁ i₁ Π (i₂ : ι₂), κ₂ i₂ Sort u_5} (f : Π (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), φ i₁ j₁ i₂ j₂) (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁) :
φ i₁ j₁ i₂ j₂

Swaps two pairs of arguments to a function.

Equations
• = λ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
def auto_param.out {α : Sort u_1} {n : name} (x : n) :
α

If `x : α . tac_name` then `x.out : α`. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to `simp`.

Equations
def opt_param.out {α : Sort u_1} {d : α} (x : α := d) :
α

If `x : α := d` then `x.out : α`. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to `simp`.

Equations

### Declarations about propositional connectives #

theorem false_ne_true  :
theorem eq_true_iff {a : Prop} :
= a

### Declarations about `implies`#

@[protected, instance]
def iff.is_refl  :
@[protected, instance]
def iff.is_trans  :
theorem iff_of_eq {a b : Prop} (e : a = b) :
a b
theorem iff_iff_eq {a b : Prop} :
a b a = b
@[simp]
theorem eq_iff_iff {p q : Prop} :
p = q (p q)
@[simp]
theorem imp_self {a : Prop} :
theorem iff.imp {a b c d : Prop} (h₁ : a b) (h₂ : c d) :
a c b d
@[simp]
theorem eq_true_eq_id  :
@[nolint]
theorem imp_intro {α β : Prop} (h : α) :
β α
theorem imp_false {a : Prop} :
theorem imp_and_distrib {b c : Prop} {α : Sort u_1} :
α b c b) c)
@[simp]
theorem and_imp {a b c : Prop} :
a b c a b c
theorem iff_def {a b : Prop} :
a b (a b) (b a)
theorem iff_def' {a b : Prop} :
a b (b a) (a b)
theorem imp_true_iff {α : Sort u_1} :
theorem imp_iff_right {a b : Prop} (ha : a) :
a b b
theorem imp_iff_not {a b : Prop} (hb : ¬b) :
a b ¬a
theorem decidable.imp_iff_right_iff {a b : Prop} [decidable a] :
a b b a b
@[simp]
theorem imp_iff_right_iff {a b : Prop} :
a b b a b
theorem decidable.and_or_imp {a b c : Prop} [decidable a] :
a b (a c) a b c
@[simp]
theorem and_or_imp {a b c : Prop} :
a b (a c) a b c
@[protected]
theorem function.mt {a b : Prop} :
(a b) ¬b ¬a

Provide modus tollens (`mt`) as dot notation for implications.

### Declarations about `not`#

def not.elim {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) :
α

Ex falso for negation. From `¬ a` and `a` anything follows. This is the same as `absurd` with the arguments flipped, but it is in the `not` namespace so that projection notation can be used.

Equations
@[reducible]
theorem not.imp {a b : Prop} (H2 : ¬b) (H1 : a b) :
theorem not_not_of_not_imp {a b : Prop} :
¬(a b) ¬¬a
theorem not_of_not_imp {b a : Prop} :
¬(a b) ¬b
@[nolint]
theorem dec_em (p : Prop) [decidable p] :
p ¬p
@[nolint]
theorem dec_em' (p : Prop) [decidable p] :
¬p p
theorem em (p : Prop) :
p ¬p
theorem em' (p : Prop) :
¬p p
theorem or_not {p : Prop} :
p ¬p
theorem decidable.eq_or_ne {α : Sort u_1} (x y : α) [decidable (x = y)] :
x = y x y
theorem decidable.ne_or_eq {α : Sort u_1} (x y : α) [decidable (x = y)] :
x y x = y
theorem eq_or_ne {α : Sort u_1} (x y : α) :
x = y x y
theorem ne_or_eq {α : Sort u_1} (x y : α) :
x y x = y
theorem by_contradiction {p : Prop} :
theorem by_contra {p : Prop} :

In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely. The `decidable` namespace contains versions of lemmas from the root namespace that explicitly attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.

You can check if a lemma uses the axiom of choice by using `#print axioms foo` and seeing if `classical.choice` appears in the list.

As mathlib is primarily classical, if the type signature of a `def` or `lemma` does not require any `decidable` instances to state, it is preferable not to introduce any `decidable` instances that are needed in the proof as arguments, but rather to use the `classical` tactic as needed.

In the other direction, when `decidable` instances do appear in the type signature, it is better to use explicitly introduced ones rather than allowing Lean to automatically infer classical ones, as these may cause instance mismatch errors later.

@[protected]
theorem decidable.not_not {a : Prop} [decidable a] :
@[simp]
theorem not_not {a : Prop} :

The Double Negation Theorem: `¬ ¬ P` is equivalent to `P`. The left-to-right direction, double negation elimination (DNE), is classically true but not constructively.

theorem of_not_not {a : Prop} :
theorem not_ne_iff {α : Sort u_1} {a b : α} :
¬a b a = b
@[protected]
theorem decidable.of_not_imp {a b : Prop} [decidable a] (h : ¬(a b)) :
a
theorem of_not_imp {a b : Prop} :
¬(a b) a
@[protected]
theorem decidable.not_imp_symm {a b : Prop} [decidable a] (h : ¬a b) (hb : ¬b) :
a
@[nolint]
theorem not.decidable_imp_symm {a b : Prop} [decidable a] :
(¬a b) ¬b a
theorem not.imp_symm {a b : Prop} :
(¬a b) ¬b a
@[protected]
theorem decidable.not_imp_comm {a b : Prop} [decidable a] [decidable b] :
¬a b ¬b a
theorem not_imp_comm {a b : Prop} :
¬a b ¬b a
@[simp]
theorem imp_not_self {a : Prop} :
a ¬a ¬a
theorem decidable.not_imp_self {a : Prop} [decidable a] :
¬a a a
@[simp]
theorem not_imp_self {a : Prop} :
¬a a a
theorem imp.swap {a b c : Prop} :
a b c b a c
theorem imp_not_comm {a b : Prop} :
a ¬b b ¬a
theorem iff.not {a b : Prop} (h : a b) :
theorem iff.not_left {a b : Prop} (h : a ¬b) :
¬a b
theorem iff.not_right {a b : Prop} (h : ¬a b) :
a ¬b
@[protected]
theorem iff.ne {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β} :
(a = b c = d) (a b c d)
theorem iff.ne_left {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β} :
(a = b c d) (a b c = d)
theorem iff.ne_right {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β} :
(a b c = d) (a = b c d)

### Declarations about `xor`#

@[simp]
theorem xor_true  :
@[simp]
theorem xor_false  :
theorem xor_comm (a b : Prop) :
xor a b xor b a
@[protected, instance]
@[simp]
theorem xor_self (a : Prop) :
xor a a = false
@[simp]
theorem xor_not_left {a b : Prop} :
xor (¬a) b (a b)
@[simp]
theorem xor_not_right {a b : Prop} :
xor a (¬b) (a b)
theorem xor_not_not {a b : Prop} :
xor (¬a) (¬b) xor a b
@[protected]
theorem xor.or {a b : Prop} (h : xor a b) :
a b

### Declarations about `and`#

theorem iff.and {a b c d : Prop} (h₁ : a b) (h₂ : c d) :
a c b d
theorem and_congr_left {a b c : Prop} (h : c (a b)) :
a c b c
theorem and_congr_left' {a b c : Prop} (h : a b) :
a c b c
theorem and_congr_right' {a b c : Prop} (h : b c) :
a b a c
theorem not_and_of_not_left {a : Prop} (b : Prop) :
¬a ¬(a b)
theorem not_and_of_not_right (a : Prop) {b : Prop} :
¬b ¬(a b)
theorem and.imp_left {a b c : Prop} (h : a b) :
a c b c
theorem and.imp_right {a b c : Prop} (h : a b) :
c a c b
theorem and.right_comm {a b c : Prop} :
(a b) c (a c) b
theorem and_and_and_comm (a b c d : Prop) :
(a b) c d (a c) b d
theorem and_and_distrib_left (a b c : Prop) :
a b c (a b) a c
theorem and_and_distrib_right (a b c : Prop) :
(a b) c (a c) b c
theorem and_rotate {a b c : Prop} :
a b c b c a
theorem and.rotate {a b c : Prop} :
a b c b c a
theorem and_not_self_iff (a : Prop) :
theorem not_and_self_iff (a : Prop) :
theorem and_iff_left_of_imp {a b : Prop} (h : a b) :
a b a
theorem and_iff_right_of_imp {a b : Prop} (h : b a) :
a b b
theorem ne_and_eq_iff_right {α : Sort u_1} {a b c : α} (h : b c) :
a b a = c a = c
@[simp]
theorem and_iff_left_iff_imp {a b : Prop} :
a b a a b
@[simp]
theorem and_iff_right_iff_imp {a b : Prop} :
a b b b a
@[simp]
theorem iff_self_and {p q : Prop} :
p p q p q
@[simp]
theorem iff_and_self {p q : Prop} :
p q p p q
@[simp]
theorem and.congr_right_iff {a b c : Prop} :
a b a c a (b c)
@[simp]
theorem and.congr_left_iff {a b c : Prop} :
a c b c c (a b)
@[simp]
theorem and_self_left {a b : Prop} :
a a b a b
@[simp]
theorem and_self_right {a b : Prop} :
(a b) b a b

### Declarations about `or`#

theorem iff.or {a b c d : Prop} (h₁ : a b) (h₂ : c d) :
a c b d
theorem or_congr_left' {a b c : Prop} (h : a b) :
a c b c
theorem or_congr_right' {a b c : Prop} (h : b c) :
a b a c
theorem or.right_comm {a b c : Prop} :
(a b) c (a c) b
theorem or_or_or_comm (a b c d : Prop) :
(a b) c d (a c) b d
theorem or_or_distrib_left (a b c : Prop) :
a b c (a b) a c
theorem or_or_distrib_right (a b c : Prop) :
(a b) c (a c) b c
theorem or_rotate {a b c : Prop} :
a b c b c a
theorem or.rotate {a b c : Prop} :
a b c b c a
theorem or_of_or_of_imp_of_imp {a b c d : Prop} (h₁ : a b) (h₂ : a c) (h₃ : b d) :
c d
theorem or_of_or_of_imp_left {a b c : Prop} (h₁ : a c) (h : a b) :
b c
theorem or_of_or_of_imp_right {a b c : Prop} (h₁ : c a) (h : a b) :
c b
theorem or.elim3 {a b c d : Prop} (h : a b c) (ha : a d) (hb : b d) (hc : c d) :
d
theorem or.imp3 {a b c d e f : Prop} (had : a d) (hbe : b e) (hcf : c f) :
a b c d e f
theorem or_imp_distrib {a b c : Prop} :
a b c (a c) (b c)
@[protected]
theorem decidable.or_iff_not_imp_left {a b : Prop} [decidable a] :
a b ¬a b
theorem or_iff_not_imp_left {a b : Prop} :
a b ¬a b
@[protected]
theorem decidable.or_iff_not_imp_right {a b : Prop} [decidable b] :
a b ¬b a
theorem or_iff_not_imp_right {a b : Prop} :
a b ¬b a
@[protected]
theorem decidable.not_or_of_imp {a b : Prop} [decidable a] (h : a b) :
¬a b
theorem not_or_of_imp {a b : Prop} :
(a b) ¬a b
@[protected]
theorem decidable.or_not_of_imp {a b : Prop} [decidable a] (h : a b) :
b ¬a
theorem or_not_of_imp {a b : Prop} :
(a b) b ¬a
@[protected]
theorem decidable.imp_iff_not_or {a b : Prop} [decidable a] :
a b ¬a b
theorem imp_iff_not_or {a b : Prop} :
a b ¬a b
@[protected]
theorem decidable.imp_iff_or_not {a b : Prop} [decidable b] :
b a a ¬b
theorem imp_iff_or_not {a b : Prop} :
b a a ¬b
@[protected]
theorem decidable.not_imp_not {a b : Prop} [decidable a] :
¬a ¬b b a
theorem not_imp_not {a b : Prop} :
¬a ¬b b a
@[protected]
theorem function.mtr {a b : Prop} :
(¬a ¬b) b a

Provide the reverse of modus tollens (`mt`) as dot notation for implications.

@[protected]
theorem decidable.or_congr_left {a b c : Prop} [decidable c] (h : ¬c (a b)) :
a c b c
theorem or_congr_left {a b c : Prop} (h : ¬c (a b)) :
a c b c
@[protected]
theorem decidable.or_congr_right {a b c : Prop} [decidable a] (h : ¬a (b c)) :
a b a c
theorem or_congr_right {a b c : Prop} (h : ¬a (b c)) :
a b a c
@[simp]
theorem or_iff_left_iff_imp {a b : Prop} :
a b a b a
@[simp]
theorem or_iff_right_iff_imp {a b : Prop} :
a b b a b
theorem or_iff_left {a b : Prop} (hb : ¬b) :
a b a
theorem or_iff_right {a b : Prop} (ha : ¬a) :
a b b

theorem and_or_distrib_left {a b c : Prop} :
a (b c) a b a c

`∧` distributes over `∨` (on the left).

theorem or_and_distrib_right {a b c : Prop} :
(a b) c a c b c

`∧` distributes over `∨` (on the right).

theorem or_and_distrib_left {a b c : Prop} :
a b c (a b) (a c)

`∨` distributes over `∧` (on the left).

theorem and_or_distrib_right {a b c : Prop} :
a b c (a c) (b c)

`∨` distributes over `∧` (on the right).

@[simp]
theorem or_self_left {a b : Prop} :
a a b a b
@[simp]
theorem or_self_right {a b : Prop} :
(a b) b a b

Declarations about `iff`

@[nolint]
theorem iff.iff {a b c d : Prop} (h₁ : a b) (h₂ : c d) :
a c (b d)
theorem iff_of_true {a b : Prop} (ha : a) (hb : b) :
a b
theorem iff_of_false {a b : Prop} (ha : ¬a) (hb : ¬b) :
a b
theorem iff_true_left {a b : Prop} (ha : a) :
a b b
theorem iff_true_right {a b : Prop} (ha : a) :
b a b
theorem iff_false_left {a b : Prop} (ha : ¬a) :
a b ¬b
theorem iff_false_right {a b : Prop} (ha : ¬a) :
b a ¬b
@[simp]
theorem iff_mpr_iff_true_intro {P : Prop} (h : P) :
_ = h
@[protected]
theorem decidable.imp_or_distrib {a b c : Prop} [decidable a] :
a b c (a b) (a c)
theorem imp_or_distrib {a b c : Prop} :
a b c (a b) (a c)
@[protected]
theorem decidable.imp_or_distrib' {a b c : Prop} [decidable b] :
a b c (a b) (a c)
theorem imp_or_distrib' {a b c : Prop} :
a b c (a b) (a c)
theorem not_imp_of_and_not {a b : Prop} :
a ¬b ¬(a b)
@[protected]
theorem decidable.not_imp {a b : Prop} [decidable a] :
¬(a b) a ¬b
theorem not_imp {a b : Prop} :
¬(a b) a ¬b
theorem imp_imp_imp {a b c d : Prop} (h₀ : c a) (h₁ : b d) :
(a b) c d
@[protected]
theorem decidable.peirce (a b : Prop) [decidable a] :
((a b) a) a
theorem peirce (a b : Prop) :
((a b) a) a
theorem peirce' {a : Prop} (H : (b : Prop), (a b) a) :
a
@[protected]
theorem decidable.not_iff_not {a b : Prop} [decidable a] [decidable b] :
¬a ¬b (a b)
theorem not_iff_not {a b : Prop} :
¬a ¬b (a b)
@[protected]
theorem decidable.not_iff_comm {a b : Prop} [decidable a] [decidable b] :
¬a b (¬b a)
theorem not_iff_comm {a b : Prop} :
¬a b (¬b a)
@[protected]
theorem decidable.not_iff {a b : Prop} [decidable b] :
¬(a b) (¬a b)
theorem not_iff {a b : Prop} :
¬(a b) (¬a b)
@[protected]
theorem decidable.iff_not_comm {a b : Prop} [decidable a] [decidable b] :
a ¬b (b ¬a)
theorem iff_not_comm {a b : Prop} :
a ¬b (b ¬a)
@[protected]
theorem decidable.iff_iff_and_or_not_and_not {a b : Prop} [decidable b] :
a b a b ¬a ¬b
theorem iff_iff_and_or_not_and_not {a b : Prop} :
a b a b ¬a ¬b
theorem decidable.iff_iff_not_or_and_or_not {a b : Prop} [decidable a] [decidable b] :
a b (¬a b) (a ¬b)
theorem iff_iff_not_or_and_or_not {a b : Prop} :
a b (¬a b) (a ¬b)
@[protected]
theorem decidable.not_and_not_right {a b : Prop} [decidable b] :
¬(a ¬b) a b
theorem not_and_not_right {a b : Prop} :
¬(a ¬b) a b
def decidable_of_iff {b : Prop} (a : Prop) (h : a b) [D : decidable a] :

Transfer decidability of `a` to decidability of `b`, if the propositions are equivalent. Important: this function should be used instead of `rw` on `decidable b`, because the kernel will get stuck reducing the usage of `propext` otherwise, and `dec_trivial` will not work.

Equations
def decidable_of_iff' {a : Prop} (b : Prop) (h : a b) [D : decidable b] :

Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent. This is the same as `decidable_of_iff` but the iff is flipped.

Equations
def decidable_of_bool {a : Prop} (b : bool) (h : b a) :

Prove that `a` is decidable by constructing a boolean `b` and a proof that `b ↔ a`. (This is sometimes taken as an alternate definition of decidability.)

Equations

### De Morgan's laws #

theorem not_and_of_not_or_not {a b : Prop} (h : ¬a ¬b) :
¬(a b)
@[protected]
theorem decidable.not_and_distrib {a b : Prop} [decidable a] :
¬(a b) ¬a ¬b
@[protected]
theorem decidable.not_and_distrib' {a b : Prop} [decidable b] :
¬(a b) ¬a ¬b
theorem not_and_distrib {a b : Prop} :
¬(a b) ¬a ¬b

One of de Morgan's laws: the negation of a conjunction is logically equivalent to the disjunction of the negations.

@[simp]
theorem not_and {a b : Prop} :
¬(a b) a ¬b
theorem not_and' {a b : Prop} :
¬(a b) b ¬a
theorem not_or_distrib {a b : Prop} :
¬(a b) ¬a ¬b

One of de Morgan's laws: the negation of a disjunction is logically equivalent to the conjunction of the negations.

@[protected]
theorem decidable.or_iff_not_and_not {a b : Prop} [decidable a] [decidable b] :
a b ¬(¬a ¬b)
theorem or_iff_not_and_not {a b : Prop} :
a b ¬(¬a ¬b)
@[protected]
theorem decidable.and_iff_not_or_not {a b : Prop} [decidable a] [decidable b] :
a b ¬(¬a ¬b)
theorem and_iff_not_or_not {a b : Prop} :
a b ¬(¬a ¬b)
@[simp]
theorem not_xor (P Q : Prop) :
¬xor P Q (P Q)
theorem xor_iff_not_iff (P Q : Prop) :
xor P Q ¬(P Q)
theorem xor_iff_iff_not {a b : Prop} :
xor a b (a ¬b)
theorem xor_iff_not_iff' {a b : Prop} :
xor a b (¬a b)

theorem ne_of_mem_of_not_mem {α : Type u_1} {β : Type u_2} [ β] {s : β} {a b : α} (h : a s) :
b s a b
theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [ β] {s t : β} {a : α} (h : a s) :
a t s t
theorem has_mem.mem.ne_of_not_mem {α : Type u_1} {β : Type u_2} [ β] {s : β} {a b : α} :
a s b s a b

Alias of `ne_of_mem_of_not_mem`.

theorem has_mem.mem.ne_of_not_mem' {α : Type u_1} {β : Type u_2} [ β] {s t : β} {a : α} :
a s a t s t

Alias of `ne_of_mem_of_not_mem'`.

@[simp]
theorem heq_iff_eq {α : Sort u_1} {a b : α} :
a == b a = b
theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) :
hp == hq
theorem ball_cond_comm {α : Sort u_1} {s : α Prop} {p : α α Prop} :
( (a : α), s a (b : α), s b p a b) (a b : α), s a s b p a b
theorem ball_mem_comm {α : out_param (Type u_1)} {β : Type u_2} [ β] {s : β} {p : α α Prop} :
( (a : α), a s (b : α), b s p a b) (a b : α), a s b s p a b
theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : α β) {x y : α} (h : f x f y) :
x y
theorem eq_equivalence {α : Sort u_1} :
@[simp]
theorem eq_rec_constant {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a') :
eq.rec y h = y

Transport through trivial families is the identity.

@[simp]
theorem eq_mp_eq_cast {α β : Sort u_1} (h : α = β) :
h.mp = cast h
@[simp]
theorem eq_mpr_eq_cast {α β : Sort u_1} (h : α = β) :
h.mpr = cast _
@[simp]
theorem cast_cast {α β γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) :
cast hb (cast ha a) = cast _ a
@[simp]
theorem congr_refl_left {α : Sort u_1} {β : Sort u_2} (f : α β) {a b : α} (h : a = b) :
_ = _
@[simp]
theorem congr_refl_right {α : Sort u_1} {β : Sort u_2} {f g : α β} (h : f = g) (a : α) :
_ = _
@[simp]
theorem congr_arg_refl {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) :
_ = _
@[simp]
theorem congr_fun_rfl {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) :
_ = _
@[simp]
theorem congr_fun_congr_arg {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β γ) {a a' : α} (p : a = a') (b : β) :
_ = _
theorem heq_of_cast_eq {α β : Sort u_1} {a : α} {a' : β} (e : α = β) (h₂ : cast e a = a') :
a == a'
theorem cast_eq_iff_heq {α β : Sort u_1} {a : α} {a' : β} {e : α = β} :
cast e a = a' a == a'
theorem rec_heq_of_heq {α : Sort u_1} {a b : α} {β : Sort u_2} {C : α Sort u_2} {x : C a} {y : β} (e : a = b) (h : x == y) :
eq.rec x e == y
theorem rec_heq_iff_heq {α : Sort u_1} {a b : α} {β : Sort u_2} {C : α Sort u_2} {x : C a} {y : β} {e : a = b} :
eq.rec x e == y x == y
theorem heq_rec_iff_heq {α : Sort u_1} {a b : α} {β : Sort u_2} {C : α Sort u_2} {x : β} {y : C a} {e : a = b} :
x == eq.rec y e x == y
@[protected]
theorem eq.congr {α : Sort u_1} {x₁ x₂ y₁ y₂ : α} (h₁ : x₁ = y₁) (h₂ : 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_arg2 {α : 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 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
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
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
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

theorem pi_congr {α : Sort u_1} {β β' : α Sort u_2} (h : (a : α), β a = β' a) :
(Π (a : α), β a) = Π (a : α), β' a
theorem forall₂_congr {α : Sort u_1} {β : α Sort u_2} {p q : Π (a : α), β a Prop} (h : (a : α) (b : β a), p a b q a b) :
( (a : α) (b : β a), p a b) (a : α) (b : β a), q a b
theorem forall₃_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {p q : Π (a : α) (b : β a), γ a b Prop} (h : (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
( (a : α) (b : β a) (c : γ a b), p a b c) (a : α) (b : β a) (c : γ a b), q a b c
theorem forall₄_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {δ : Π (a : α) (b : β a), γ a b Sort u_4} {p q : Π (a : α) (b : β a) (c : γ a b), δ a b c Prop} (h : (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d q a b c d) :
( (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d
theorem forall₅_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {δ : Π (a : α) (b : β a), γ a b Sort u_4} {ε : Π (a : α) (b : β a) (c : γ a b), δ a b c Sort u_5} {p q : Π (a : α) (b : β a) (c : γ a b) (d : δ a b c), ε a b c d Prop} (h : (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e q a b c d e) :
( (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e
theorem exists₂_congr {α : Sort u_1} {β : α Sort u_2} {p q : Π (a : α), β a Prop} (h : (a : α) (b : β a), p a b q a b) :
( (a : α) (b : β a), p a b) (a : α) (b : β a), q a b
theorem exists₃_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {p q : Π (a : α) (b : β a), γ a b Prop} (h : (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
( (a : α) (b : β a) (c : γ a b), p a b c) (a : α) (b : β a) (c : γ a b), q a b c
theorem exists₄_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {δ : Π (a : α) (b : β a), γ a b Sort u_4} {p q : Π (a : α) (b : β a) (c : γ a b), δ a b c Prop} (h : (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d q a b c d) :
( (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d) (a : α) (b : β a) (c : γ a b) (d : δ a b c), q a b c d
theorem exists₅_congr {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {δ : Π (a : α) (b : β a), γ a b Sort u_4} {ε : Π (a : α) (b : β a) (c : γ a b), δ a b c Sort u_5} {p q : Π (a : α) (b : β a) (c : γ a b) (d : δ a b c), ε a b c d Prop} (h : (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e q a b c d e) :
( (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e) (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), q a b c d e
theorem forall_imp {α : Sort u_1} {p q : α Prop} (h : (a : α), p a q a) :
( (a : α), p a) (a : α), q a
theorem forall₂_imp {α : Sort u_1} {β : α Sort u_2} {p q : Π (a : α), β a Prop} (h : (a : α) (b : β a), p a b q a b) :
( (a : α) (b : β a), p a b) (a : α) (b : β a), q a b
theorem forall₃_imp {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {p q : Π (a : α) (b : β a), γ a b Prop} (h : (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
( (a : α) (b : β a) (c : γ a b), p a b c) (a : α) (b : β a) (c : γ a b), q a b c
theorem Exists.imp {α : Sort u_1} {p q : α Prop} (h : (a : α), p a q a) :
( (a : α), p a) ( (a : α), q a)
theorem Exists₂.imp {α : Sort u_1} {β : α Sort u_2} {p q : Π (a : α), β a Prop} (h : (a : α) (b : β a), p a b q a b) :
( (a : α) (b : β a), p a b) ( (a : α) (b : β a), q a b)
theorem Exists₃.imp {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} {p q : Π (a : α) (b : β a), γ a b Prop} (h : (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
( (a : α) (b : β a) (c : γ a b), p a b c) ( (a : α) (b : β a) (c : γ a b), q a b c)
theorem exists_imp_exists' {α : Sort u_1} {β : Sort u_3} {p : α Prop} {q : β Prop} (f : α β) (hpq : (a : α), p a q (f a)) (hp : (a : α), p a) :
(b : β), q b
theorem forall_swap {α : Sort u_1} {β : Sort u_3} {p : α β Prop} :
( (x : α) (y : β), p x y) (y : β) (x : α), p x y
theorem forall₂_swap {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁ Sort u_3} {κ₂ : ι₂ Sort u_4} {p : Π (i₁ : ι₁), κ₁ i₁ Π (i₂ : ι₂), κ₂ i₂ Prop} :
( (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
theorem imp_forall_iff {α : Type u_1} {p : Prop} {q : α Prop} :
p (x : α), q x (x : α), p q x

We intentionally restrict the type of `α` in this lemma so that this is a safer to use in simp than `forall_swap`.

theorem exists_swap {α : Sort u_1} {β : Sort u_3} {p : α β Prop} :
( (x : α) (y : β), p x y) (y : β) (x : α), p x y
@[simp]
theorem forall_exists_index {α : Sort u_1} {p : α Prop} {q : ( (x : α), p x) Prop} :
( (h : (x : α), p x), q h) (x : α) (h : p x), q _
theorem exists_imp_distrib {α : Sort u_1} {p : α Prop} {b : Prop} :
( (x : α), p x) b (x : α), p x b
@[reducible]
noncomputable def Exists.some {α : Sort u_1} {p : α Prop} (P : (a : α), p a) :
α

Extract an element from a existential statement, using `classical.some`.

Equations
theorem Exists.some_spec {α : Sort u_1} {p : α Prop} (P : (a : α), p a) :
p P.some

Show that an element extracted from `P : ∃ a, p a` using `P.some` satisfies `p`.

theorem not_exists_of_forall_not {α : Sort u_1} {p : α Prop} (h : (x : α), ¬p x) :
¬ (x : α), p x
@[simp]
theorem not_exists {α : Sort u_1} {p : α Prop} :
(¬ (x : α), p x) (x : α), ¬p x
theorem not_forall_of_exists_not {α : Sort u_1} {p : α Prop} :
( (x : α), ¬p x) (¬ (x : α), p x)
@[protected]
theorem decidable.not_forall {α : Sort u_1} {p : α Prop} [decidable ( (x : α), ¬p x)] [Π (x : α), decidable (p x)] :
(¬ (x : α), p x) (x : α), ¬p x
@[simp]
theorem not_forall {α : Sort u_1} {p : α Prop} :
(¬ (x : α), p x) (x : α), ¬p x
@[protected]
theorem decidable.not_forall_not {α : Sort u_1} {p : α Prop} [decidable ( (x : α), p x)] :
(¬ (x : α), ¬p x) (x : α), p x
theorem not_forall_not {α : Sort u_1} {p : α Prop} :
(¬ (x : α), ¬p x) (x : α), p x
@[protected]
theorem decidable.not_exists_not {α : Sort u_1} {p : α Prop} [Π (x : α), decidable (p x)] :
(¬ (x : α), ¬p x) (x : α), p x
@[simp]
theorem not_exists_not {α : Sort u_1} {p : α Prop} :
(¬ (x : α), ¬p x) (x : α), p x
theorem forall_imp_iff_exists_imp {α : Sort u_1} {p : α Prop} {b : Prop} [ha : nonempty α] :
( (x : α), p x) b (x : α), p x b
theorem forall_true_iff {α : Sort u_1} :
theorem forall_true_iff' {α : Sort u_1} {p : α Prop} (h : (a : α), p a true) :
( (a : α), p a) true
@[simp]
theorem forall_2_true_iff {α : Sort u_1} {β : α Sort u_2} :
( (a : α), β a true) true
@[simp]
theorem forall_3_true_iff {α : Sort u_1} {β : α Sort u_2} {γ : Π (a : α), β a Sort u_3} :
( (a : α) (b : β a), γ a b true) true
theorem exists_unique.exists {α : Sort u_1} {p : α Prop} (h : ∃! (x : α), p x) :
(x : α), p x
@[simp]
theorem exists_unique_iff_exists {α : Sort u_1} [subsingleton α] {p : α Prop} :
(∃! (x : α), p x) (x : α), p x
@[simp]
theorem forall_const {b : Prop} (α : Sort u_1) [i : nonempty α] :
α b b
@[simp]
theorem forall_forall_const {α : Type u_1} {β : Type u_2} (p : β Prop) [nonempty α] :
( (x : β), α p x) (x : β), p x

For some reason simp doesn't use `forall_const` to simplify in this case.

@[simp]
theorem exists_const {b : Prop} (α : Sort u_1) [i : nonempty α] :
( (x : α), b) b
theorem exists_unique_const {b : Prop} (α : Sort u_1) [i : nonempty α] [subsingleton α] :
(∃! (x : α), b) b
theorem forall_and_distrib {α : Sort u_1} {p q : α Prop} :
( (x : α), p x q x) ( (x : α), p x) (x : α), q x
theorem exists_or_distrib {α : Sort u_1} {p q : α Prop} :
( (x : α), p x q x) ( (x : α), p x) (x : α), q x
@[simp]
theorem exists_and_distrib_left {α : Sort u_1} {q : Prop} {p : α Prop} :
( (x : α), q p x) q (x : α), p x
@[simp]
theorem exists_and_distrib_right {α : Sort u_1} {q : Prop} {p : α Prop} :
( (x : α), p x q) ( (x : α), p x) q
@[simp]
theorem forall_eq {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), a = a' p a) p a'
@[simp]
theorem forall_eq' {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), a' = a p a) p a'
theorem decidable.and_forall_ne {α : Sort u_1} {p : α Prop} [decidable_eq α] (a : α) :
(p a (b : α), b a p b) (b : α), p b
theorem and_forall_ne {α : Sort u_1} {p : α Prop} (a : α) :
(p a (b : α), b a p b) (b : α), p b
@[simp]
theorem forall_eq_or_imp {α : Sort u_1} {p q : α Prop} {a' : α} :
( (a : α), a = a' q a p a) p a' (a : α), q a p a
theorem ne.ne_or_ne {α : Sort u_1} {x y : α} (z : α) (h : x y) :
x z y z
theorem exists_eq {α : Sort u_1} {a' : α} :
(a : α), a = a'
@[simp]
theorem exists_eq' {α : Sort u_1} {a' : α} :
(a : α), a' = a
@[simp]
theorem exists_unique_eq {α : Sort u_1} {a' : α} :
∃! (a : α), a = a'
@[simp]
theorem exists_unique_eq' {α : Sort u_1} {a' : α} :
∃! (a : α), a' = a
@[simp]
theorem exists_eq_left {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), a = a' p a) p a'
@[simp]
theorem exists_eq_right {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), p a a = a') p a'
@[simp]
theorem exists_eq_right_right {α : Sort u_1} {p q : α Prop} {a' : α} :
( (a : α), p a q a a = a') p a' q a'
@[simp]
theorem exists_eq_right_right' {α : Sort u_1} {p q : α Prop} {a' : α} :
( (a : α), p a q a a' = a) p a' q a'
@[simp]
theorem exists_apply_eq_apply {α : Sort u_1} {β : Sort u_3} (f : α β) (a' : α) :
(a : α), f a = f a'
@[simp]
theorem exists_apply_eq_apply' {α : Sort u_1} {β : Sort u_3} (f : α β) (a' : α) :
(a : α), f a' = f a
@[simp]
theorem exists_exists_and_eq_and {α : Sort u_1} {β : Sort u_3} {f : α β} {p : α Prop} {q : β Prop} :
( (b : β), ( (a : α), p a f a = b) q b) (a : α), p a q (f a)
@[simp]
theorem exists_exists_eq_and {α : Sort u_1} {β : Sort u_3} {f : α β} {p : β Prop} :
( (b : β), ( (a : α), f a = b) p b) (a : α), p (f a)
@[simp]
theorem exists_or_eq_left {α : Sort u_1} (y : α) (p : α Prop) :
(x : α), x = y p x
@[simp]
theorem exists_or_eq_right {α : Sort u_1} (y : α) (p : α Prop) :
(x : α), p x x = y
@[simp]
theorem exists_or_eq_left' {α : Sort u_1} (y : α) (p : α Prop) :
(x : α), y = x p x
@[simp]
theorem exists_or_eq_right' {α : Sort u_1} (y : α) (p : α Prop) :
(x : α), p x y = x
@[simp]
theorem forall_apply_eq_imp_iff {α : Sort u_1} {β : Sort u_3} {f : α β} {p : β Prop} :
( (a : α) (b : β), f a = b p b) (a : α), p (f a)
@[simp]
theorem forall_apply_eq_imp_iff' {α : Sort u_1} {β : Sort u_3} {f : α β} {p : β Prop} :
( (b : β) (a : α), f a = b p b) (a : α), p (f a)
@[simp]
theorem forall_eq_apply_imp_iff {α : Sort u_1} {β : Sort u_3} {f : α β} {p : β Prop} :
( (a : α) (b : β), b = f a p b) (a : α), p (f a)
@[simp]
theorem forall_eq_apply_imp_iff' {α : Sort u_1} {β : Sort u_3} {f : α β} {p : β Prop} :
( (b : β) (a : α), b = f a p b) (a : α), p (f a)
@[simp]
theorem forall_apply_eq_imp_iff₂ {α : Sort u_1} {β : Sort u_3} {f : α β} {p : α Prop} {q : β Prop} :
( (b : β) (a : α), p a f a = b q b) (a : α), p a q (f a)
@[simp]
theorem exists_eq_left' {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), a' = a p a) p a'
@[simp]
theorem exists_eq_right' {α : Sort u_1} {p : α Prop} {a' : α} :
( (a : α), p a a' = a) p a'
theorem exists_comm {α : Sort u_1} {β : Sort u_3} {p : α β Prop} :
( (a : α) (b : β), p a b) (b : β) (a : α), p a b
theorem exists₂_comm {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁ Sort u_3} {κ₂ : ι₂ Sort u_4} {p : Π (i₁ : ι₁), κ₁ i₁ Π (i₂ : ι₂), κ₂ i₂ Prop} :
( (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
theorem and.exists {p q : Prop} {f : p q Prop} :
( (h : p q), f h) (hp : p) (hq : q), f _
theorem forall_or_of_or_forall {α : Sort u_1} {p : α Prop} {b : Prop} (h : b (x : α), p x) (x : α) :
b p x
@[protected]
theorem decidable.forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α Prop} [decidable q] :
( (x : α), q p x) q (x : α), p x
theorem forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α Prop} :
( (x : α), q p x) q (x : α), p x
@[protected]
theorem decidable.forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α Prop} [decidable q] :
( (x : α), p x q) ( (x : α), p x) q
theorem forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α Prop} :
( (x : α), p x q) ( (x : α), p x) q
@[simp]
theorem exists_prop {p q : Prop} :
( (h : p), q) p q
theorem exists_unique_prop {p q : Prop} :
(∃! (h : p), q) p q
@[simp]
theorem exists_false {α : Sort u_1} :
¬ (a : α), false
@[simp]
theorem exists_unique_false {α : Sort u_1} :
¬∃! (a : α), false
theorem Exists.fst {b : Prop} {p : b Prop} :
b
theorem Exists.snd {b : Prop} {p : b Prop} (h : Exists p) :
p _
theorem forall_prop_of_true {p : Prop} {q : p Prop} (h : p) :
( (h' : p), q h') q h
theorem exists_prop_of_true {p : Prop} {q : p Prop} (h : p) :
( (h' : p), q h') q h
theorem exists_iff_of_forall {p : Prop} {q : p Prop} (h : (h : p), q h) :
( (h : p), q h) p
theorem exists_unique_prop_of_true {p : Prop} {q : p Prop} (h : p) :
(∃! (h' : p), q h') q h
theorem forall_prop_of_false {p : Prop} {q : p Prop} (hn : ¬p) :
( (h' : p), q h') true
theorem exists_prop_of_false {p : Prop} {q : p Prop} :
¬p (¬ (h' : p), q h')
theorem exists_prop_congr {p p' : Prop} {q q' : p Prop} (hq : (h : p), q h q' h) (hp : p p') :
(h : p'), q' _
theorem exists_prop_congr' {p p' : Prop} {q q' : p Prop} (hq : (h : p), q h q' h) (hp : p p') :
= (h : p'), q' _
@[simp]
theorem exists_true_left (p : true Prop) :
( (x : true), p x) p true.intro

See `is_empty.exists_iff` for the `false` version.

theorem exists_unique.unique {α : Sort u_1} {p : α Prop} (h : ∃! (x : α), p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) :
y₁ = y₂
theorem forall_prop_congr {p p' : Prop} {q q' : p Prop} (hq : (h : p), q h q' h) (hp : p p') :
( (h : p), q h) (h : p'), q' _
theorem forall_prop_congr' {p p' : Prop} {q q' : p Prop} (hq : (h : p), q h q' h) (hp : p p') :
( (h : p), q h) = (h : p'), q' _
@[simp]
theorem forall_true_left (p : true Prop) :
( (x : true), p x) p true.intro

See `is_empty.forall_iff` for the `false` version.

theorem exists_unique.elim2 {α : Sort u_1} {p : α Sort u_2} [ (x : α), subsingleton (p x)] {q : Π (x : α), p x Prop} {b : Prop} (h₂ : ∃! (x : α) (h : p x), q x h) (h₁ : (x : α) (h : p x), q x h ( (y : α) (hy : p y), q y hy y = x) b) :
b
theorem exists_unique.intro2 {α : Sort u_1} {p : α Sort u_2} [ (x : α), subsingleton (p x)] {q : Π (x : α), p x Prop} (w : α) (hp : p w) (hq : q w hp) (H : (y : α) (hy : p y), q y hy y = w) :
∃! (x : α) (hx : p x), q x hx
theorem exists_unique.exists2 {α : Sort u_1} {p : α Sort u_2} {q : Π (x : α), p x Prop} (h : ∃! (x : α) (hx : p x), q x hx) :
(x : α) (hx : p x), q x hx
theorem exists_unique.unique2 {α : Sort u_1} {p : α Sort u_2} [ (x : α), subsingleton (p x)] {q : Π (x : α), p x Prop} (h : ∃! (x : α) (hx : p x), q x hx) {y₁ y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) :
y₁ = y₂

### Classical lemmas #

theorem classical.cases {p : Prop Prop} (h1 : p true) (h2 : p false) (a : Prop) :
p a
noncomputable def classical.dec (p : Prop) :

Any prop `p` is decidable classically. A shorthand for `classical.prop_decidable`.

Equations
noncomputable def classical.dec_pred {α : Sort u_1} (p : α Prop) :

Any predicate `p` is decidable classically.

Equations
• = λ (a : α),
noncomputable def classical.dec_rel {α : Sort u_1} (p : α α Prop) :

Any relation `p` is decidable classically.

Equations
noncomputable def classical.dec_eq (α : Sort u_1) :

Any type `α` has decidable equality classically.

Equations
• = λ (a b : α),
noncomputable def classical.exists_cases {α : Sort u_1} {p : α Prop} {C : Sort u} (H0 : C) (H : Π (a : α), p a C) :
C

Construct a function from a default value `H0`, and a function to use if there exists a value satisfying the predicate.

Equations
• = dite ( (a : α), p a) (λ (h : (a : α), p a), H _) (λ (h : ¬ (a : α), p a), H0)
theorem classical.some_spec2 {α : Sort u_1} {p : α Prop} {h : (a : α), p a} (q : α Prop) (hpq : (a : α), p a q a) :
q
noncomputable def classical.subtype_of_exists {α : Type u_1} {P : α Prop} (h : (x : α), P x) :
{x // P x}

A version of classical.indefinite_description which is definitionally equal to a pair

Equations
@[protected]
noncomputable def classical.by_contradiction' {α : Sort u_1} (H : ¬ false)) :
α

A version of `by_contradiction` that uses types instead of propositions.

Equations
def classical.choice_of_by_contradiction' {α : Sort u_1} (contra : ¬ false) α) :
α

`classical.by_contradiction'` is equivalent to lean's axiom `classical.choice`.

Equations
noncomputable def exists.classical_rec_on {α : Sort u_1} {p : α Prop} (h : (a : α), p a) {C : Sort u} (H : Π (a : α), p a C) :
C

This function has the same type as `exists.rec_on`, and can be used to case on an equality, but `exists.rec_on` can only eliminate into Prop, while this version eliminates into any universe using the axiom of choice.

Equations
• = H _

### Declarations about bounded quantifiers #

theorem bex_def {α : Sort u_1} {p q : α Prop} :
( (x : α) (h : p x), q x) (x : α), p x q x
theorem bex.elim {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} {b : Prop} :
( (x : α) (h : p x), P x h) ( (a : α) (h : p a), P a h b) b
theorem bex.intro {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} (a : α) (h₁ : p a) (h₂ : P a h₁) :
(x : α) (h : p x), P x h
theorem ball_congr {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} (H : (x : α) (h : p x), P x h Q x h) :
( (x : α) (h : p x), P x h) (x : α) (h : p x), Q x h
theorem bex_congr {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} (H : (x : α) (h : p x), P x h Q x h) :
( (x : α) (h : p x), P x h) (x : α) (h : p x), Q x h
theorem bex_eq_left {α : Sort u_1} {p : α Prop} {a : α} :
( (x : α) (_x : x = a), p x) p a
theorem ball.imp_right {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} (H : (x : α) (h : p x), P x h Q x h) (h₁ : (x : α) (h : p x), P x h) (x : α) (h : p x) :
Q x h
theorem bex.imp_right {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} (H : (x : α) (h : p x), P x h Q x h) :
( (x : α) (h : p x), P x h) ( (x : α) (h : p x), Q x h)
theorem ball.imp_left {α : Sort u_1} {r p q : α Prop} (H : (x : α), p x q x) (h₁ : (x : α), q x r x) (x : α) (h : p x) :
r x
theorem bex.imp_left {α : Sort u_1} {r p q : α Prop} (H : (x : α), p x q x) :
( (x : α) (_x : p x), r x) ( (x : α) (_x : q x), r x)
theorem ball_of_forall {α : Sort u_1} {p : α Prop} (h : (x : α), p x) (x : α) :
p x
theorem forall_of_ball {α : Sort u_1} {p q : α Prop} (H : (x : α), p x) (h : (x : α), p x q x) (x : α) :
q x
theorem bex_of_exists {α : Sort u_1} {p q : α Prop} (H : (x : α), p x) :
( (x : α), q x) ( (x : α) (_x : p x), q x)
theorem exists_of_bex {α : Sort u_1} {p q : α Prop} :
( (x : α) (_x : p x), q x) ( (x : α), q x)
@[simp]
theorem bex_imp_distrib {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} {b : Prop} :
( (x : α) (h : p x), P x h) b (x : α) (h : p x), P x h b
theorem not_bex {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} :
(¬ (x : α) (h : p x), P x h) (x : α) (h : p x), ¬P x h
theorem not_ball_of_bex_not {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} :
( (x : α) (h : p x), ¬P x h) (¬ (x : α) (h : p x), P x h)
@[protected]
theorem decidable.not_ball {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} [decidable ( (x : α) (h : p x), ¬P x h)] [Π (x : α) (h : p x), decidable (P x h)] :
(¬ (x : α) (h : p x), P x h) (x : α) (h : p x), ¬P x h
theorem not_ball {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} :
(¬ (x : α) (h : p x), P x h) (x : α) (h : p x), ¬P x h
theorem ball_true_iff {α : Sort u_1} (p : α Prop) :
( (x : α), p x true) true
theorem ball_and_distrib {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} :
( (x : α) (h : p x), P x h Q x h) ( (x : α) (h : p x), P x h) (x : α) (h : p x), Q x h
theorem bex_or_distrib {α : Sort u_1} {p : α Prop} {P Q : Π (x : α), p x Prop} :
( (x : α) (h : p x), P x h Q x h) ( (x : α) (h : p x), P x h) (x : α) (h : p x), Q x h
theorem ball_or_left_distrib {α : Sort u_1} {r p q : α Prop} :
( (x : α), p x q x r x) ( (x : α), p x r x) (x : α), q x r x
theorem bex_or_left_distrib {α : Sort u_1} {r p q : α Prop} :
( (x : α) (_x : p x q x), r x) ( (x : α) (_x : p x), r x) (x : α) (_x : q x), r x
theorem classical.not_ball {α : Sort u_1} {p : α Prop} {P : Π (x : α), p x Prop} :
(¬ (x : α) (h : p x), P x h) (x : α) (h : p x), ¬P x h
theorem dite_eq_iff {α : Sort u_1} {P : Prop} [decidable P] {c : α} {A : P α} {B : ¬P α} :
dite P A B = c ( (h : P), A h = c) (h : ¬P), B h = c
theorem ite_eq_iff {α : Sort u_1} {P : Prop} [decidable P] {a b c : α} :
ite P a b = c P a = c ¬P b = c
theorem dite_eq_iff' {α : Sort u_1} {P : Prop} [decidable P] {c : α} {A : P α} {B : ¬P α} :
dite P A B = c ( (h : P), A h = c) (h : ¬P), B h = c
theorem ite_eq_iff' {α : Sort u_1} {P : Prop} [decidable P] {a b c : α} :
ite P a b = c (P a = c) (¬P b = c)
@[simp]
theorem dite_eq_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a : α} {B : ¬P α} :
dite P (λ (_x : P), a) B = a (h : ¬P), B h = a
@[simp]
theorem dite_eq_right_iff {α : Sort u_1} {P : Prop} [decidable P] {b : α} {A : P α} :
dite P A (λ (_x : ¬P), b) = b (h : P), A h = b
@[simp]
theorem ite_eq_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b = a ¬P b = a
@[simp]
theorem ite_eq_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b = b P a = b
theorem dite_ne_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a : α} {B : ¬P α} :
dite P (λ (_x : P), a) B a (h : ¬P), a B h
theorem dite_ne_right_iff {α : Sort u_1} {P : Prop} [decidable P] {b : α} {A : P α} :
dite P A (λ (_x : ¬P), b) b (h : P), A h b
theorem ite_ne_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b a ¬P a b
theorem ite_ne_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b b P a b
@[protected]
theorem ne.dite_eq_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a : α} {B : ¬P α} (h : (h : ¬P), a B h) :
dite P (λ (_x : P), a) B = a P
@[protected]
theorem ne.dite_eq_right_iff {α : Sort u_1} {P : Prop} [decidable P] {b : α} {A : P α} (h : (h : P), A h b) :
dite P A (λ (_x : ¬P), b) = b ¬P
@[protected]
theorem ne.ite_eq_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} (h : a b) :
ite P a b = a P
@[protected]
theorem ne.ite_eq_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} (h : a b) :
ite P a b = b ¬P
@[protected]
theorem ne.dite_ne_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a : α} {B : ¬P α} (h : (h : ¬P), a B h) :
dite P (λ (_x : P), a) B a ¬P
@[protected]
theorem ne.dite_ne_right_iff {α : Sort u_1} {P : Prop} [decidable P] {b : α} {A : P α} (h : (h : P), A h b) :
dite P A (λ (_x : ¬P), b) b P
@[protected]
theorem ne.ite_ne_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} (h : a b) :
ite P a b a ¬P
@[protected]
theorem ne.ite_ne_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} (h : a b) :
ite P a b b P
@[simp]
theorem dite_eq_ite {α : Sort u_1} (P : Prop) [decidable P] (a b : α) :
dite P (λ (h : P), a) (λ (h : ¬P), b) = ite P a b

A `dite` whose results do not actually depend on the condition may be reduced to an `ite`.

theorem dite_eq_or_eq {α : Sort u_1} (P : Prop) [decidable P] {A : P α} {B : ¬P α} :
( (h : P), dite P A B = A h) (h : ¬P), dite P A B = B h
theorem ite_eq_or_eq {α : Sort u_1} (P : Prop) [decidable P] (a b : α) :
ite P a b = a ite P a b = b
theorem apply_dite {α : Sort u_1} {β : Sort u_2} (f : α β) (P : Prop) [decidable P] (x : P α) (y : ¬P α) :
f (dite P x y) = dite P (λ (h : P), f (x h)) (λ (h : ¬P), f (y h))

A function applied to a `dite` is a `dite` of that function applied to each of the branches.

theorem apply_ite {α : Sort u_1} {β : Sort u_2} (f : α β) (P : Prop) [decidable P] (a b : α) :
f (ite P a b) = ite P (f a) (f b)

A function applied to a `ite` is a `ite` of that function applied to each of the branches.

theorem apply_dite2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β γ) (P : Prop) [decidable P] (a : P α) (b : ¬P α) (c : P β) (d : ¬P β) :
f (dite P a b) (dite P c d) = dite P (λ (h : P), f (a h) (c h)) (λ (h : ¬P), f (b h) (d h))

A two-argument function applied to two `dite`s is a `dite` of that two-argument function applied to each of the branches.

theorem apply_ite2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β γ) (P : Prop) [decidable P] (a b : α) (c d : β) :
f (ite P a b) (ite P c d) = ite P (f a c) (f b d)

A two-argument function applied to two `ite`s is a `ite` of that two-argument function applied to each of the branches.

theorem dite_apply {α : Sort u_1} {σ : α Sort u_4} (P : Prop) [decidable P] (f : P Π (a : α), σ a) (g : ¬P Π (a : α), σ a) (a : α) :
dite P f g a = dite P (λ (h : P), f h a) (λ (h : ¬P), g h a)

A 'dite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `dite` that applies either branch to `a`.

theorem ite_apply {α : Sort u_1} {σ : α Sort u_4} (P : Prop) [decidable P] (f g : Π (a : α), σ a) (a : α) :
ite P f g a = ite P (f a) (g a)

A 'ite' producing a `Pi` type `Π a, σ a`, applied to a value `a : α` is a `ite` that applies either branch to `a`.

@[simp]
theorem dite_not {α : Sort u_1} (P : Prop) [decidable P] (x : ¬P α) (y : ¬¬P α) :
dite (¬P) x y = dite P (λ (h : P), y _) x

Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches.

@[simp]
theorem ite_not {α : Sort u_1} (P : Prop) [decidable P] (a b : α) :
ite (¬P) a b = ite P b a

Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches.

theorem ite_and {α : Sort u_1} (P Q : Prop) [decidable P] [decidable Q] (a b : α) :
ite (P Q) a b = ite P (ite Q a b) b
theorem dite_dite_comm {α : Sort u_1} (P Q : Prop) [decidable P] [decidable Q] {A : P α} {B : Q α} {C : ¬P ¬Q α} (h : P ¬Q) :
dite P (λ (p : P), A p) (λ (p : ¬P), dite Q (λ (q : Q), B q) (λ (q : ¬Q), C p q)) = dite Q (λ (q : Q), B q) (λ (q : ¬Q), dite P (λ (p : P), A p) (λ (p : ¬P), C p q))
theorem ite_ite_comm {α : Sort u_1} (P Q : Prop) [decidable P] [decidable Q] (a b : α) {c : α} (h : P ¬Q) :
ite P a (ite Q b c) = ite Q b (ite P a c)