mathlib documentation

logic.basic

Basic logic properties #

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.

source
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
source
def empty.elim {C : Sort u_1} :
empty → C

Ex falso, the nondependent eliminator for the empty type.

source
@[protected, instance]
def empty.subsingleton  :
subsingleton empty
source
@[protected, instance]
def subsingleton.prod {α : Type u_1} {β : Type u_2} [subsingleton α] [subsingleton β] :
subsingleton (α × β)
source
@[protected, instance]
def empty.decidable_eq  :
decidable_eq empty
Equations
source
@[protected, instance]
def sort.inhabited  :
inhabited (Sort u_1)
Equations
source
@[protected, instance]
def sort.inhabited'  :
inhabited (default (Sort u_1))
Equations
source
@[protected, instance]
def psum.inhabited_left {α : Sort u_1} {β : Sort u_2} [inhabited α] :
inhabited (psum α β)
Equations
source
@[protected, instance]
def psum.inhabited_right {α : Sort u_1} {β : Sort u_2} [inhabited β] :
inhabited (psum α β)
Equations
source
@[protected, instance]
def decidable_eq_of_subsingleton {α : Sort u_1} [subsingleton α] :
decidable_eq α
Equations
source
@[simp]
theorem eq_iff_true_of_subsingleton {α : Sort u_1} [subsingleton α] (x y : α) :
x = y ↔ true
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 subtype.subsingleton (α : Sort u_1) [subsingleton α] (p : α → Prop) :
subsingleton (subtype p)
source
@[simp]
theorem coe_coe {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [has_coe α β] [has_coe_t β γ] (a : α) :
↑a = ↑↑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.

source
theorem coe_fn_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : out_param (γ → Sort u_4)} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ δ] (x : α) :
⇑x = ⇑↑x
source
theorem coe_fn_coe_trans' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : out_param (Sort u_4)} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ (λ (_x : γ), δ)] (x : α) :
⇑x = ⇑↑x

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

source
@[simp]
theorem coe_fn_coe_base {α : Sort u_1} {β : Sort u_2} {γ : out_param (β → Sort u_3)} [has_coe α β] [has_coe_to_fun β γ] (x : α) :
⇑x = ⇑↑x
source
theorem coe_fn_coe_base' {α : Sort u_1} {β : Sort u_2} {γ : out_param (Sort u_3)} [has_coe α β] [has_coe_to_fun β (λ (_x : β), γ)] (x : α) :
⇑x = ⇑↑x

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

source
theorem coe_sort_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : out_param (Sort u_4)} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ δ] (x : α) :
↥x = ↥↑x
source
@[simp]
theorem coe_sort_coe_base {α : Sort u_1} {β : Sort u_2} {γ : out_param (Sort u_3)} [has_coe α β] [has_coe_to_sort β γ] (x : α) :
↥x = ↥↑x
source
@[nolint]
inductive pempty  :
Sort u

pempty is the universe-polymorphic analogue of empty.

source
@[protected, instance]
def pempty.decidable_eq  :
decidable_eq pempty
source
def pempty.elim {C : Sort u_1} :
pempty → C

Ex falso, the nondependent eliminator for the pempty type.

source
@[protected, instance]
def subsingleton_pempty  :
subsingleton pempty
source
@[simp]
theorem not_nonempty_pempty  :
¬nonempty pempty
source
@[simp]
theorem forall_pempty {P : pempty → Prop} :
(∀ (x : pempty), P x) ↔ true
source
@[simp]
theorem exists_pempty {P : pempty → Prop} :
(∃ (x : pempty), P x) ↔ false
source
theorem congr_arg_heq {α : Sort u_1} {β : α → Sort u_2} (f : Π (a : α), β a) {a₁ a₂ : α} :
a₁ = a₂ → f a₁ == f a₂
source
theorem plift.down_inj {α : Sort u_1} (a b : plift α) :
a.down = b.down → a = b
source
theorem ne_comm {α : Sort u_1} {a b : α} :
a ≠ b ↔ b ≠ a
source
@[simp]
theorem eq_iff_eq_cancel_left {α : Type u_1} {b c : α} :
(∀ {a : α}, a = b ↔ a = c) ↔ b = c
source
@[simp]
theorem eq_iff_eq_cancel_right {α : Type u_1} {a b : α} :
(∀ {c : α}, a = c ↔ b = c) ↔ a = b
source
@[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
source
theorem fact.elim {p : Prop} (h : fact p) :
p
source
theorem fact_iff {p : Prop} :
fact p ↔ p

Declarations about propositional connectives #

source
theorem false_ne_true  :
false ≠ true

Declarations about implies #

source
@[protected, instance]
def iff.is_refl  :
is_refl Prop iff
source
@[protected, instance]
def iff.is_trans  :
is_trans Prop iff
source
theorem iff_of_eq {a b : Prop} (e : a = b) :
a ↔ b
source
theorem iff_iff_eq {a b : Prop} :
a ↔ b ↔ a = b
source
@[simp]
theorem eq_iff_iff {p q : Prop} :
p = q ↔ (p ↔ q)
source
@[simp]
theorem imp_self {a : Prop} :
a → a ↔ true
source
@[nolint]
theorem imp_intro {α β : Prop} (h : α) :
β → α
source
theorem imp_false {a : Prop} :
a → false ↔ ¬a
source
theorem imp_and_distrib {b c : Prop} {α : Sort u_1} :
α → b ∧ c ↔ (α → b) ∧ (α → c)
source
@[simp]
theorem and_imp {a b c : Prop} :
a ∧ b → c ↔ a → b → c
source
theorem iff_def {a b : Prop} :
a ↔ b ↔ (a → b) ∧ (b → a)
source
theorem iff_def' {a b : Prop} :
a ↔ b ↔ (b → a) ∧ (a → b)
source
theorem imp_true_iff {α : Sort u_1} :
α → true ↔ true
source
theorem imp_iff_right {a b : Prop} (ha : a) :
a → b ↔ b
source
theorem imp_iff_not {a b : Prop} (hb : ¬b) :
a → b ↔ ¬a
source
theorem decidable.imp_iff_right_iff {a b : Prop} [decidable a] :
a → b ↔ b ↔ a ∨ b
source
@[simp]
theorem imp_iff_right_iff {a b : Prop} :
a → b ↔ b ↔ a ∨ b
source
theorem decidable.and_or_imp {a b c : Prop} [decidable a] :
a ∧ b ∨ (a → c) ↔ a → b ∨ c
source
@[simp]
theorem and_or_imp {a b c : Prop} :
a ∧ b ∨ (a → c) ↔ a → b ∨ c

Declarations about not #

source
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
source
theorem not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) :
¬a
source
theorem not_not_of_not_imp {a b : Prop} :
¬(a → b) → ¬¬a
source
theorem not_of_not_imp {b a : Prop} :
¬(a → b) → ¬b
source
@[nolint]
theorem dec_em (p : Prop) [decidable p] :
p ∨ ¬p
source
@[nolint]
theorem dec_em' (p : Prop) [decidable p] :
¬p ∨ p
source
theorem em (p : Prop) :
p ∨ ¬p
source
theorem em' (p : Prop) :
¬p ∨ p
source
theorem or_not {p : Prop} :
p ∨ ¬p
source
theorem decidable.eq_or_ne {α : Sort u_1} (x y : α) [decidable (x = y)] :
x = y ∨ x ≠ y
source
theorem decidable.ne_or_eq {α : Sort u_1} (x y : α) [decidable (x = y)] :
x ≠ y ∨ x = y
source
theorem eq_or_ne {α : Sort u_1} (x y : α) :
x = y ∨ x ≠ y
source
theorem ne_or_eq {α : Sort u_1} (x y : α) :
x ≠ y ∨ x = y
source
theorem by_contradiction {p : Prop} :
(¬p → false) → p
source
theorem by_contra {p : Prop} :
(¬p → false) → p
source
@[protected]
theorem decidable.not_not {a : Prop} [decidable a] :
¬¬a ↔ a
source
@[simp]
theorem not_not {a : Prop} :
¬¬a ↔ a

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

source
theorem of_not_not {a : Prop} :
¬¬a → a
source
@[protected]
theorem decidable.of_not_imp {a b : Prop} [decidable a] (h : ¬(a → b)) :
a
source
theorem of_not_imp {a b : Prop} :
¬(a → b) → a
source
@[protected]
theorem decidable.not_imp_symm {a b : Prop} [decidable a] (h : ¬a → b) (hb : ¬b) :
a
source
@[nolint]
theorem not.decidable_imp_symm {a b : Prop} [decidable a] :
(¬a → b) → ¬b → a
source
theorem not.imp_symm {a b : Prop} :
(¬a → b) → ¬b → a
source
@[protected]
theorem decidable.not_imp_comm {a b : Prop} [decidable a] [decidable b] :
¬a → b ↔ ¬b → a
source
theorem not_imp_comm {a b : Prop} :
¬a → b ↔ ¬b → a
source
@[simp]
theorem imp_not_self {a : Prop} :
a → ¬a ↔ ¬a
source
theorem decidable.not_imp_self {a : Prop} [decidable a] :
¬a → a ↔ a
source
@[simp]
theorem not_imp_self {a : Prop} :
¬a → a ↔ a
source
theorem imp.swap {a b c : Prop} :
a → b → c ↔ b → a → c
source
theorem imp_not_comm {a b : Prop} :
a → ¬b ↔ b → ¬a

Declarations about xor #

source
@[simp]
theorem xor_true  :
xor true = not
source
@[simp]
theorem xor_false  :
xor false = id
source
theorem xor_comm (a b : Prop) :
xor a b = xor b a
source
@[protected, instance]
def xor.is_commutative  :
is_commutative Prop xor
source
@[simp]
theorem xor_self (a : Prop) :
xor a a = false

Declarations about and #

source
theorem and_congr_left {a b c : Prop} (h : c → (a ↔ b)) :
a ∧ c ↔ b ∧ c
source
theorem and_congr_left' {a b c : Prop} (h : a ↔ b) :
a ∧ c ↔ b ∧ c
source
theorem and_congr_right' {a b c : Prop} (h : b ↔ c) :
a ∧ b ↔ a ∧ c
source
theorem not_and_of_not_left {a : Prop} (b : Prop) :
¬a → ¬(a ∧ b)
source
theorem not_and_of_not_right (a : Prop) {b : Prop} :
¬b → ¬(a ∧ b)
source
theorem and.imp_left {a b c : Prop} (h : a → b) :
a ∧ c → b ∧ c
source
theorem and.imp_right {a b c : Prop} (h : a → b) :
c ∧ a → c ∧ b
source
theorem and.right_comm {a b c : Prop} :
(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
source
theorem and_and_and_comm (a b c d : Prop) :
(a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
source
theorem and.rotate {a b c : Prop} :
a ∧ b ∧ c ↔ b ∧ c ∧ a
source
theorem and_not_self_iff (a : Prop) :
a ∧ ¬a ↔ false
source
theorem not_and_self_iff (a : Prop) :
¬a ∧ a ↔ false
source
theorem and_iff_left_of_imp {a b : Prop} (h : a → b) :
a ∧ b ↔ a
source
theorem and_iff_right_of_imp {a b : Prop} (h : b → a) :
a ∧ b ↔ b
source
@[simp]
theorem and_iff_left_iff_imp {a b : Prop} :
a ∧ b ↔ a ↔ a → b
source
@[simp]
theorem and_iff_right_iff_imp {a b : Prop} :
a ∧ b ↔ b ↔ b → a
source
@[simp]
theorem iff_self_and {p q : Prop} :
p ↔ p ∧ q ↔ p → q
source
@[simp]
theorem iff_and_self {p q : Prop} :
p ↔ q ∧ p ↔ p → q
source
@[simp]
theorem and.congr_right_iff {a b c : Prop} :
a ∧ b ↔ a ∧ c ↔ a → (b ↔ c)
source
@[simp]
theorem and.congr_left_iff {a b c : Prop} :
a ∧ c ↔ b ∧ c ↔ c → (a ↔ b)
source
@[simp]
theorem and_self_left {a b : Prop} :
a ∧ a ∧ b ↔ a ∧ b
source
@[simp]
theorem and_self_right {a b : Prop} :
(a ∧ b) ∧ b ↔ a ∧ b

Declarations about or #

source
theorem or_congr_left {a b c : Prop} (h : a ↔ b) :
a ∨ c ↔ b ∨ c
source
theorem or_congr_right {a b c : Prop} (h : b ↔ c) :
a ∨ b ↔ a ∨ c
source
theorem or.right_comm {a b c : Prop} :
(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b
source
theorem or_of_or_of_imp_of_imp {a b c d : Prop} (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) :
c ∨ d
source
theorem or_of_or_of_imp_left {a b c : Prop} (h₁ : a ∨ c) (h : a → b) :
b ∨ c
source
theorem or_of_or_of_imp_right {a b c : Prop} (h₁ : c ∨ a) (h : a → b) :
c ∨ b
source
theorem or.elim3 {a b c d : Prop} (h : a ∨ b ∨ c) (ha : a → d) (hb : b → d) (hc : c → d) :
d
source
theorem or_imp_distrib {a b c : Prop} :
a ∨ b → c ↔ (a → c) ∧ (b → c)
source
@[protected]
theorem decidable.or_iff_not_imp_left {a b : Prop} [decidable a] :
a ∨ b ↔ ¬a → b
source
theorem or_iff_not_imp_left {a b : Prop} :
a ∨ b ↔ ¬a → b
source
@[protected]
theorem decidable.or_iff_not_imp_right {a b : Prop} [decidable b] :
a ∨ b ↔ ¬b → a
source
theorem or_iff_not_imp_right {a b : Prop} :
a ∨ b ↔ ¬b → a
source
@[protected]
theorem decidable.not_imp_not {a b : Prop} [decidable a] :
¬a → ¬b ↔ b → a
source
theorem not_imp_not {a b : Prop} :
¬a → ¬b ↔ b → a
source
@[simp]
theorem or_iff_left_iff_imp {a b : Prop} :
a ∨ b ↔ a ↔ b → a
source
@[simp]
theorem or_iff_right_iff_imp {a b : Prop} :
a ∨ b ↔ b ↔ a → b

Declarations about distributivity #

source
theorem and_or_distrib_left {a b c : Prop} :
a ∧ (b ∨ c) ↔ a ∧ b ∨ a ∧ c

∧ distributes over ∨ (on the left).

source
theorem or_and_distrib_right {a b c : Prop} :
(a ∨ b) ∧ c ↔ a ∧ c ∨ b ∧ c

∧ distributes over ∨ (on the right).

source
theorem or_and_distrib_left {a b c : Prop} :
a ∨ b ∧ c ↔ (a ∨ b) ∧ (a ∨ c)

∨ distributes over ∧ (on the left).

source
theorem and_or_distrib_right {a b c : Prop} :
a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)

∨ distributes over ∧ (on the right).

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

Declarations about iff

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

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
source
def decidable_of_iff' {a : Prop} (b : Prop) (h : a ↔ b) [D : decidable b] :
decidable a

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
source
def decidable_of_bool {a : Prop} (b : bool) (h : ↥b ↔ a) :
decidable 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 #

source
theorem not_and_of_not_or_not {a b : Prop} (h : ¬a ∨ ¬b) :
¬(a ∧ b)
source
@[protected]
theorem decidable.not_and_distrib {a b : Prop} [decidable a] :
¬(a ∧ b) ↔ ¬a ∨ ¬b
source
@[protected]
theorem decidable.not_and_distrib' {a b : Prop} [decidable b] :
¬(a ∧ b) ↔ ¬a ∨ ¬b
source
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.

source
@[simp]
theorem not_and {a b : Prop} :
¬(a ∧ b) ↔ a → ¬b
source
theorem not_and' {a b : Prop} :
¬(a ∧ b) ↔ b → ¬a
source
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.

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

Declarations about equality #

source
@[simp]
theorem heq_iff_eq {α : Sort u_1} {a b : α} :
a == b ↔ a = b
source
theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) :
hp == hq
source
theorem ne_of_mem_of_not_mem {α : out_param (Type u_1)} {β : Type u_2} [has_mem α β] {s : β} {a b : α} (h : a ∈ s) :
b ∉ s → a ≠ b
source
theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : α → β) {x y : α} (h : f x ≠ f y) :
x ≠ y
source
theorem eq_equivalence {α : Sort u_1} :
equivalence eq
source
@[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.

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

Declarations about quantifiers #

source
theorem forall_imp {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a → q a) :
(∀ (a : α), p a) → ∀ (a : α), q a
source
theorem forall₂_congr {α : Sort u_1} {β : Sort u_2} {p q : α → β → Prop} (h : ∀ (a : α) (b : β), p a b ↔ q a b) :
(∀ (a : α) (b : β), p a b) ↔ ∀ (a : α) (b : β), q a b
source
theorem forall₃_congr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p q : α → β → γ → Prop} (h : ∀ (a : α) (b : β) (c : γ), p a b c ↔ q a b c) :
(∀ (a : α) (b : β) (c : γ), p a b c) ↔ ∀ (a : α) (b : β) (c : γ), q a b c
source
theorem forall₄_congr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {p q : α → β → γ → δ → Prop} (h : ∀ (a : α) (b : β) (c : γ) (d : δ), p a b c d ↔ q a b c d) :
(∀ (a : α) (b : β) (c : γ) (d : δ), p a b c d) ↔ ∀ (a : α) (b : β) (c : γ) (d : δ), q a b c d
source
theorem Exists.imp {α : Sort u_1} {q p : α → Prop} (h : ∀ (a : α), p a → q a) (p_1 : ∃ (a : α), p a) :
∃ (a : α), q a
source
theorem exists_imp_exists' {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (hpq : ∀ (a : α), p a → q (f a)) (hp : ∃ (a : α), p a) :
∃ (b : β), q b
source
theorem exists₂_congr {α : Sort u_1} {β : Sort u_2} {p q : α → β → Prop} (h : ∀ (a : α) (b : β), p a b ↔ q a b) :
(∃ (a : α) (b : β), p a b) ↔ ∃ (a : α) (b : β), q a b
source
theorem exists₃_congr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p q : α → β → γ → Prop} (h : ∀ (a : α) (b : β) (c : γ), p a b c ↔ q a b c) :
(∃ (a : α) (b : β) (c : γ), p a b c) ↔ ∃ (a : α) (b : β) (c : γ), q a b c
source
theorem exists₄_congr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {p q : α → β → γ → δ → Prop} (h : ∀ (a : α) (b : β) (c : γ) (d : δ), p a b c d ↔ q a b c d) :
(∃ (a : α) (b : β) (c : γ) (d : δ), p a b c d) ↔ ∃ (a : α) (b : β) (c : γ) (d : δ), q a b c d
source
theorem forall_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
source
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.

source
theorem exists_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∃ (x : α) (y : β), p x y) ↔ ∃ (y : β) (x : α), p x y
source
@[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 _
source
theorem exists_imp_distrib {α : Sort u_1} {p : α → Prop} {b : Prop} :
(∃ (x : α), p x) → b ↔ ∀ (x : α), p x → b
source
noncomputable def Exists.some {α : Sort u_1} {p : α → Prop} (P : ∃ (a : α), p a) :
α

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

Equations
source
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.

source
theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} (h : ∀ (x : α), ¬p x) :
¬∃ (x : α), p x
source
@[simp]
theorem not_exists {α : Sort u_1} {p : α → Prop} :
(¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x
source
theorem not_forall_of_exists_not {α : Sort u_1} {p : α → Prop} :
(∃ (x : α), ¬p x) → (¬∀ (x : α), p x)
source
@[protected]
theorem decidable.not_forall {α : Sort u_1} {p : α → Prop} [decidable (∃ (x : α), ¬p x)] [Π (x : α), decidable (p x)] :
(¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x
source
@[simp]
theorem not_forall {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x
source
@[protected]
theorem decidable.not_forall_not {α : Sort u_1} {p : α → Prop} [decidable (∃ (x : α), p x)] :
(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x
source
theorem not_forall_not {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x
source
@[protected]
theorem decidable.not_exists_not {α : Sort u_1} {p : α → Prop} [Π (x : α), decidable (p x)] :
(¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x
source
@[simp]
theorem not_exists_not {α : Sort u_1} {p : α → Prop} :
(¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x
source
theorem forall_imp_iff_exists_imp {α : Sort u_1} {p : α → Prop} {b : Prop} [ha : nonempty α] :
(∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
source
theorem forall_true_iff {α : Sort u_1} :
α → true ↔ true
source
theorem forall_true_iff' {α : Sort u_1} {p : α → Prop} (h : ∀ (a : α), p a ↔ true) :
(∀ (a : α), p a) ↔ true
source
@[simp]
theorem forall_2_true_iff {α : Sort u_1} {β : α → Sort u_2} :
(∀ (a : α), β a → true) ↔ true
source
@[simp]
theorem forall_3_true_iff {α : Sort u_1} {β : α → Sort u_2} {γ : Π (a : α), β a → Sort u_3} :
(∀ (a : α) (b : β a), γ a b → true) ↔ true
source
theorem exists_unique.exists {α : Sort u_1} {p : α → Prop} (h : ∃! (x : α), p x) :
∃ (x : α), p x
source
@[simp]
theorem exists_unique_iff_exists {α : Sort u_1} [subsingleton α] {p : α → Prop} :
(∃! (x : α), p x) ↔ ∃ (x : α), p x
source
@[simp]
theorem forall_const {b : Prop} (α : Sort u_1) [i : nonempty α] :
α → b ↔ b
source
@[simp]
theorem exists_const {b : Prop} (α : Sort u_1) [i : nonempty α] :
(∃ (x : α), b) ↔ b
source
theorem exists_unique_const {b : Prop} (α : Sort u_1) [i : nonempty α] [subsingleton α] :
(∃! (x : α), b) ↔ b
source
theorem forall_and_distrib {α : Sort u_1} {p q : α → Prop} :
(∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
source
theorem exists_or_distrib {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α), p x ∨ q x) ↔ (∃ (x : α), p x) ∨ ∃ (x : α), q x
source
@[simp]
theorem exists_and_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∃ (x : α), q ∧ p x) ↔ q ∧ ∃ (x : α), p x
source
@[simp]
theorem exists_and_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∃ (x : α), p x ∧ q) ↔ (∃ (x : α), p x) ∧ q
source
@[simp]
theorem forall_eq {α : Sort u_1} {p : α → Prop} {a' : α} :
(∀ (a : α), a = a' → p a) ↔ p a'
source
@[simp]
theorem forall_eq' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∀ (a : α), a' = a → p a) ↔ p a'
source
theorem and_forall_ne {α : Sort u_1} {p : α → Prop} (a : α) :
(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
source
@[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
source
theorem exists_eq {α : Sort u_1} {a' : α} :
∃ (a : α), a = a'
source
@[simp]
theorem exists_eq' {α : Sort u_1} {a' : α} :
∃ (a : α), a' = a
source
@[simp]
theorem exists_unique_eq {α : Sort u_1} {a' : α} :
∃! (a : α), a = a'
source
@[simp]
theorem exists_unique_eq' {α : Sort u_1} {a' : α} :
∃! (a : α), a' = a
source
@[simp]
theorem exists_eq_left {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), a = a' ∧ p a) ↔ p a'
source
@[simp]
theorem exists_eq_right {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ a = a') ↔ p a'
source
@[simp]
theorem exists_eq_right_right {α : Sort u_1} {p : α → Prop} {b : Prop} {a' : α} :
(∃ (a : α), p a ∧ b ∧ a = a') ↔ p a' ∧ b
source
@[simp]
theorem exists_eq_right_right' {α : Sort u_1} {p : α → Prop} {b : Prop} {a' : α} :
(∃ (a : α), p a ∧ b ∧ a' = a) ↔ p a' ∧ b
source
@[simp]
theorem exists_apply_eq_apply {α : Sort u_1} {β : Sort u_2} (f : α → β) (a' : α) :
∃ (a : α), f a = f a'
source
@[simp]
theorem exists_apply_eq_apply' {α : Sort u_1} {β : Sort u_2} (f : α → β) (a' : α) :
∃ (a : α), f a' = f a
source
@[simp]
theorem exists_exists_and_eq_and {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : α → Prop} {q : β → Prop} :
(∃ (b : β), (∃ (a : α), p a ∧ f a = b) ∧ q b) ↔ ∃ (a : α), p a ∧ q (f a)
source
@[simp]
theorem exists_exists_eq_and {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :
(∃ (b : β), (∃ (a : α), f a = b) ∧ p b) ↔ ∃ (a : α), p (f a)
source
@[simp]
theorem exists_or_eq_left {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), x = y ∨ p x
source
@[simp]
theorem exists_or_eq_right {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), p x ∨ x = y
source
@[simp]
theorem exists_or_eq_left' {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), y = x ∨ p x
source
@[simp]
theorem exists_or_eq_right' {α : Sort u_1} (y : α) (p : α → Prop) :
∃ (x : α), p x ∨ y = x
source
@[simp]
theorem forall_apply_eq_imp_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :
(∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_apply_eq_imp_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :
(∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_eq_apply_imp_iff {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :
(∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_eq_apply_imp_iff' {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :
(∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)
source
@[simp]
theorem forall_apply_eq_imp_iff₂ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : α → Prop} {q : β → Prop} :
(∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)
source
@[simp]
theorem exists_eq_left' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), a' = a ∧ p a) ↔ p a'
source
@[simp]
theorem exists_eq_right' {α : Sort u_1} {p : α → Prop} {a' : α} :
(∃ (a : α), p a ∧ a' = a) ↔ p a'
source
theorem exists_comm {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∃ (a : α) (b : β), p a b) ↔ ∃ (b : β) (a : α), p a b
source
theorem and.exists {p q : Prop} {f : p ∧ q → Prop} :
(∃ (h : p ∧ q), f h) ↔ ∃ (hp : p) (hq : q), f _
source
theorem forall_or_of_or_forall {α : Sort u_1} {p : α → Prop} {b : Prop} (h : b ∨ ∀ (x : α), p x) (x : α) :
b ∨ p x
source
@[protected]
theorem decidable.forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} [decidable q] :
(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
source
theorem forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
source
@[protected]
theorem decidable.forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} [decidable q] :
(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
source
theorem forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
source
@[simp]
theorem exists_prop {p q : Prop} :
(∃ (h : p), q) ↔ p ∧ q
source
theorem exists_unique_prop {p q : Prop} :
(∃! (h : p), q) ↔ p ∧ q
source
@[simp]
theorem exists_false {α : Sort u_1} :
¬∃ (a : α), false
source
@[simp]
theorem exists_unique_false {α : Sort u_1} :
¬∃! (a : α), false
source
theorem Exists.fst {b : Prop} {p : b → Prop} :
Exists p → b
source
theorem Exists.snd {b : Prop} {p : b → Prop} (h : Exists p) :
p _
source
theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∀ (h' : p), q h') ↔ q h
source
theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∃ (h' : p), q h') ↔ q h
source
theorem exists_unique_prop_of_true {p : Prop} {q : p → Prop} (h : p) :
(∃! (h' : p), q h') ↔ q h
source
theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) :
(∀ (h' : p), q h') ↔ true
source
theorem exists_prop_of_false {p : Prop} {q : p → Prop} :
¬p → (¬∃ (h' : p), q h')
source
theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') :
Exists q ↔ ∃ (h : p'), q' _
source
theorem exists_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') :
Exists q = ∃ (h : p'), q' _
source
@[simp]
theorem exists_true_left (p : true → Prop) :
(∃ (x : true), p x) ↔ p true.intro
source
@[simp]
theorem exists_false_left (p : false → Prop) :
¬∃ (x : false), p x
source
theorem exists_unique.unique {α : Sort u_1} {p : α → Prop} (h : ∃! (x : α), p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) :
y₁ = y₂
source
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' _
source
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' _
source
@[simp]
theorem forall_true_left (p : true → Prop) :
(∀ (x : true), p x) ↔ p true.intro
source
@[simp]
theorem forall_false_left (p : false → Prop) :
(∀ (x : false), p x) ↔ true
source
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
source
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
source
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
source
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 #

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

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

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

Any predicate p is decidable classically.

Equations
source
noncomputable def classical.dec_rel {α : Sort u_1} (p : α → α → Prop) :
decidable_rel p

Any relation p is decidable classically.

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

Any type α has decidable equality classically.

Equations
source
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
source
theorem classical.some_spec2 {α : Sort u_1} {p : α → Prop} {h : ∃ (a : α), p a} (q : α → Prop) (hpq : ∀ (a : α), p a → q a) :
q (classical.some h)
source
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
source
@[protected]
noncomputable def classical.by_contradiction' {α : Sort u_1} (H : ¬(α → false)) :
α

A version of by_contradiction that uses types instead of propositions.

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

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

Equations
source
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

Declarations about bounded quantifiers #

source
theorem bex_def {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α) (h : p x), q x) ↔ ∃ (x : α), p x ∧ q x
source
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
source
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
source
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
source
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
source
theorem bex_eq_left {α : Sort u_1} {p : α → Prop} {a : α} :
(∃ (x : α) (_x : x = a), p x) ↔ p a
source
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
source
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)
source
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
source
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)
source
theorem ball_of_forall {α : Sort u_1} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) :
p x
source
theorem forall_of_ball {α : Sort u_1} {p q : α → Prop} (H : ∀ (x : α), p x) (h : ∀ (x : α), p x → q x) (x : α) :
q x
source
theorem bex_of_exists {α : Sort u_1} {p q : α → Prop} (H : ∀ (x : α), p x) :
(∃ (x : α), q x) → (∃ (x : α) (_x : p x), q x)
source
theorem exists_of_bex {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α) (_x : p x), q x) → (∃ (x : α), q x)
source
@[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
source
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
source
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)
source
@[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
source
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
source
theorem ball_true_iff {α : Sort u_1} (p : α → Prop) :
(∀ (x : α), p x → true) ↔ true
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem ite_eq_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b = a ↔ ¬P → b = a
source
@[simp]
theorem ite_eq_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b = b ↔ P → a = b
source
theorem ite_ne_left_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b ≠ a ↔ ¬P ∧ a ≠ b
source
theorem ite_ne_right_iff {α : Sort u_1} {P : Prop} [decidable P] {a b : α} :
ite P a b ≠ b ↔ P ∧ a ≠ b
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem ite_eq_or_eq {α : Sort u_1} (P : Prop) [decidable P] (a b : α) :
ite P a b = a ∨ ite P a b = b
source
@[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.

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

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

source
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 dites is a dite of that two-argument function applied to each of the branches.

source
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 ites is a ite of that two-argument function applied to each of the branches.

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

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

source
@[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.

source
@[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.

source
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