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.

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

• hidden = a

instance decidableEq_of_subsingleton {α : Sort u_1} [Subsingleton α] : DecidableEq α

Equations

• decidableEq_of_subsingleton a b = isTrue (_ : a = b)

instance instSubsingletonSubtype (α : Sort u_1) [Subsingleton α] (p : α → Prop) : Subsingleton (Subtype p)

Equations

• (_ : Subsingleton (Subtype p)) = (_ : Subsingleton (Subtype p))

theorem congr_heq {α : Sort u_1} {β : Sort u_1} {γ : Sort u_2} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y

theorem congr_arg_heq {α : Sort u_2} {β : α → Sort u_1} (f : (a : α) → β a) {a₁ : α} {a₂ : α} : a₁ = a₂ → HEq (f a₁) (f a₂)

theorem ULift.down_injective {α : Type u_1} : Function.Injective ULift.down

@[simp]

theorem ULift.down_inj {α : Type u_1} {a : ULift.{u_2, u_1} α} {b : ULift.{u_2, u_1} α} : a.down = b.down ↔ a = b

theorem PLift.down_injective {α : Sort u_1} : Function.Injective PLift.down

@[simp]

theorem PLift.down_inj {α : Sort u_1} {a : PLift α} {b : PLift α} : a.down = b.down ↔ a = b

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

theorem ne_and_eq_iff_right {α : Sort u_1} {a : α} {b : α} {c : α} (h : b ≠ c) : a ≠ b ∧ a = c ↔ a = c

class Fact (p : Prop) : Prop

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.

• out : p

  Fact.out contains the unwrapped witness for the fact represented by the instance of Fact p.

theorem Fact.elim {p : Prop} (h : Fact p) : p

theorem fact_iff {p : Prop} : Fact p ↔ p

@[reducible]

def Function.swap₂ {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁ → Sort u_1} {κ₂ : ι₂ → Sort u_2} {φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort u_3} (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

• Function.swap₂ f i₂ j₂ i₁ j₁ = f i₁ j₁ i₂ j₂

Declarations about propositional connectives

Declarations about implies

instance instIsReflPropIff : IsRefl Prop Iff

Equations

• instIsReflPropIff = (_ : IsRefl Prop Iff)

instance instIsTransPropIff : IsTrans Prop Iff

Equations

• instIsTransPropIff = (_ : IsTrans Prop Iff)

theorem Iff.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a → b ↔ c → d

Alias of imp_congr.

@[simp]

theorem eq_true_eq_id : Eq True = id

@[simp]

theorem imp_iff_right_iff {a : Prop} {b : Prop} : (a → b ↔ b) ↔ a ∨ b

@[simp]

theorem and_or_imp {a : Prop} {b : Prop} {c : Prop} : a ∧ b ∨ (a → c) ↔ a → b ∨ c

theorem Function.mt {a : Prop} {b : Prop} : (a → b) → ¬b → ¬a

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

Declarations about not

theorem dec_em (p : Prop) [Decidable p] : p ∨ ¬p

Alias of Decidable.em.

theorem dec_em' (p : Prop) [Decidable p] : ¬p ∨ p

theorem em (p : Prop) : p ∨ ¬p

Alias of Classical.em.

---

Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.

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} : (¬p → False) → p

theorem by_cases {p : Prop} {q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q

theorem by_contra {p : Prop} : (¬p → False) → p

Alias of by_contradiction.

theorem of_not_not {a : Prop} : ¬¬a → a

theorem not_ne_iff : ∀ {α : Sort u_1} {a b : α}, ¬a ≠ b ↔ a = b

theorem of_not_imp {a : Prop} {b : Prop} : ¬(a → b) → a

theorem Not.decidable_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬a → b) (hb : ¬b) : a

Alias of Decidable.not_imp_symm.

theorem Not.imp_symm {a : Prop} {b : Prop} : (¬a → b) → ¬b → a

theorem not_imp_comm {a : Prop} {b : Prop} : ¬a → b ↔ ¬b → a

@[simp]

theorem not_imp_self {a : Prop} : ¬a → a ↔ a

theorem Imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} : a → b → c ↔ b → a → c

theorem Iff.not {a : Prop} {b : Prop} (h : a ↔ b) : ¬a ↔ ¬b

Alias of not_congr.

theorem Iff.not_left {a : Prop} {b : Prop} (h : a ↔ ¬b) : ¬a ↔ b

theorem Iff.not_right {a : Prop} {b : Prop} (h : ¬a ↔ b) : a ↔ ¬b

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 : Xor' True = Not

@[simp]

theorem xor_false : Xor' False = id

theorem xor_comm (a : Prop) (b : Prop) : Xor' a b = Xor' b a

instance instCommutativePropXor' : Std.Commutative Xor'

Equations

• instCommutativePropXor' = (_ : Std.Commutative Xor')

@[simp]

theorem xor_self (a : Prop) : Xor' a a = False

@[simp]

theorem xor_not_left {a : Prop} {b : Prop} : Xor' (¬a) b ↔ (a ↔ b)

@[simp]

theorem xor_not_right {a : Prop} {b : Prop} : Xor' a ¬b ↔ (a ↔ b)

theorem xor_not_not {a : Prop} {b : Prop} : Xor' (¬a) ¬b ↔ Xor' a b

theorem Xor'.or {a : Prop} {b : Prop} (h : Xor' a b) : a ∨ b

Declarations about and

theorem Iff.and {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d

Alias of and_congr.

theorem And.rotate {a : Prop} {b : Prop} {c : Prop} : a ∧ b ∧ c → b ∧ c ∧ a

Alias of the forward direction of and_rotate.

theorem and_symm_right {α : Sort u_1} (a : α) (b : α) (p : Prop) : p ∧ a = b ↔ p ∧ b = a

theorem and_symm_left {α : Sort u_1} (a : α) (b : α) (p : Prop) : a = b ∧ p ↔ b = a ∧ p

Declarations about or

theorem Iff.or {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a ∨ b ↔ c ∨ d

Alias of or_congr.

theorem Or.rotate {a : Prop} {b : Prop} {c : Prop} : a ∨ b ∨ c → b ∨ c ∨ a

Alias of the forward direction of or_rotate.

@[deprecated Or.imp]

theorem or_of_or_of_imp_of_imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) : c ∨ d

@[deprecated Or.imp_left]

theorem or_of_or_of_imp_left {a : Prop} {c : Prop} {b : Prop} (h₁ : a ∨ c) (h : a → b) : b ∨ c

@[deprecated Or.imp_right]

theorem or_of_or_of_imp_right {c : Prop} {a : Prop} {b : Prop} (h₁ : c ∨ a) (h : a → b) : c ∨ b

theorem Or.elim3 {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h : a ∨ b ∨ c) (ha : a → d) (hb : b → d) (hc : c → d) : d

theorem Or.imp3 {a : Prop} {d : Prop} {b : Prop} {e : Prop} {c : Prop} {f : Prop} (had : a → d) (hbe : b → e) (hcf : c → f) : a ∨ b ∨ c → d ∨ e ∨ f

theorem not_or_of_imp {a : Prop} {b : Prop} : (a → b) → ¬a ∨ b

theorem Decidable.or_not_of_imp {a : Prop} {b : Prop} [Decidable a] (h : a → b) : b ∨ ¬a

theorem or_not_of_imp {a : Prop} {b : Prop} : (a → b) → b ∨ ¬a

theorem imp_iff_not_or {a : Prop} {b : Prop} : a → b ↔ ¬a ∨ b

theorem imp_iff_or_not {b : Prop} {a : Prop} : b → a ↔ a ∨ ¬b

theorem not_imp_not {a : Prop} {b : Prop} : ¬a → ¬b ↔ b → a

@[simp]

theorem imp_and_neg_imp_iff (p : Prop) (q : Prop) : (p → q) ∧ (¬p → q) ↔ q

theorem Function.mtr {a : Prop} {b : Prop} : (¬a → ¬b) → b → a

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

theorem or_congr_left' {c : Prop} {a : Prop} {b : Prop} (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c

theorem or_congr_right' {a : Prop} {b : Prop} {c : Prop} (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c

Declarations about distributivity

Declarations about iff

theorem Iff.iff {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d)

Alias of iff_congr.

theorem iff_mpr_iff_true_intro {P : Prop} (h : P) : (_ : P) = h

theorem imp_or {a : Prop} {b : Prop} {c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem imp_or' {a : Sort u_1} {b : Prop} {c : Prop} : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem not_imp {a : Prop} {b : Prop} : ¬(a → b) ↔ a ∧ ¬b

theorem peirce (a : Prop) (b : Prop) : ((a → b) → a) → a

theorem not_iff_not {a : Prop} {b : Prop} : (¬a ↔ ¬b) ↔ (a ↔ b)

theorem not_iff_comm {a : Prop} {b : Prop} : (¬a ↔ b) ↔ (¬b ↔ a)

theorem not_iff {a : Prop} {b : Prop} : ¬(a ↔ b) ↔ (¬a ↔ b)

theorem iff_not_comm {a : Prop} {b : Prop} : (a ↔ ¬b) ↔ (b ↔ ¬a)

theorem iff_iff_and_or_not_and_not {a : Prop} {b : Prop} : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

theorem iff_iff_not_or_and_or_not {a : Prop} {b : Prop} : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

theorem not_and_not_right {a : Prop} {b : Prop} : ¬(a ∧ ¬b) ↔ a → b

De Morgan's laws

theorem not_and_or {a : Prop} {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.

theorem or_iff_not_and_not {a : Prop} {b : Prop} : a ∨ b ↔ ¬(¬a ∧ ¬b)

theorem and_iff_not_or_not {a : Prop} {b : Prop} : a ∧ b ↔ ¬(¬a ∨ ¬b)

@[simp]

theorem not_xor (P : Prop) (Q : Prop) : ¬Xor' P Q ↔ (P ↔ Q)

theorem xor_iff_not_iff (P : Prop) (Q : Prop) : Xor' P Q ↔ ¬(P ↔ Q)

theorem xor_iff_iff_not {a : Prop} {b : Prop} : Xor' a b ↔ (a ↔ ¬b)

theorem xor_iff_not_iff' {a : Prop} {b : Prop} : Xor' a b ↔ (¬a ↔ b)

Declarations about equality

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

Alias of ne_of_mem_of_not_mem.

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

Alias of ne_of_mem_of_not_mem'.

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 {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {p : α → α → Prop} : (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → p a b) ↔ ∀ (a b : α), a ∈ s → b ∈ s → p a b

theorem eq_equivalence {α : Sort u_1} : Equivalence Eq

theorem congr_refl_left {α : Sort u_1} {β : Sort u_2} (f : α → β) {a : α} {b : α} (h : a = b) : (_ : f a = f b) = (_ : f a = f b)

theorem congr_refl_right {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : α → β} (h : f = g) (a : α) : (_ : f a = g a) = (_ : f a = g a)

theorem congr_arg_refl {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α) : (_ : f a = f a) = (_ : f a = f a)

theorem congr_fun_rfl {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α) : (_ : f a = f a) = (_ : f a = f a)

theorem congr_fun_congr_arg {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {a : α} {a' : α} (p : a = a') (b : β) : (_ : f a b = f a' b) = (_ : f a b = f a' b)

theorem Eq.rec_eq_cast {α : Sort u_1} {P : α → Sort u_2} {x : α} {y : α} (h : x = y) (z : P x) : h ▸ z = cast (_ : P x = P y) z

theorem eqRec_heq' {α : Sort u_1} {a' : α} {motive : (a : α) → a' = a → Sort u} (p : motive a' (_ : a' = a')) {a : α} (t : a' = a) : HEq (t ▸ p) p

theorem rec_heq_of_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : α → Sort u_1} {x : C a} {y : β} (e : a = b) (h : HEq x y) : HEq (e ▸ x) y

theorem rec_heq_iff_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : α → Sort u_1} {x : C a} {y : β} {e : a = b} : HEq (e ▸ x) y ↔ HEq x y

theorem heq_rec_iff_heq {α : Sort u_2} {β : Sort u_1} {a : α} {b : α} {C : α → Sort u_1} {x : β} {y : C a} {e : a = b} : HEq x (e ▸ y) ↔ HEq x y

Declarations about quantifiers

theorem pi_congr {α : Sort u_5} {β : α → Sort u_1} {β' : α → Sort u_1} (h : ∀ (a : α), β a = β' a) : ((a : α) → β a) = ((a : α) → β' a)

theorem forall₂_imp {α : Sort u_5} {β : α → Sort u_1} {p : (a : α) → β a → Prop} {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_5} {β : α → Sort u_1} {γ : (a : α) → β a → Sort u_2} {p : (a : α) → (b : β a) → γ a b → Prop} {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_5} {β : α → Sort u_1} {p : (a : α) → β a → Prop} {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_5} {β : α → Sort u_1} {γ : (a : α) → β a → Sort u_2} {p : (a : α) → (b : β a) → γ a b → Prop} {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_swap {α : Sort u_3} {β : Sort u_2} {p : α → β → Prop} : (∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y

theorem forall₂_swap {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁ → Sort u_2} {κ₂ : ι₂ → Sort u_3} {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_2} {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_3} {β : Sort u_2} {p : α → β → Prop} : (∃ (x : α), ∃ (y : β), p x y) ↔ ∃ (y : β), ∃ (x : α), p x y

theorem not_forall_not {α : Sort u_2} {p : α → Prop} : (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

theorem forall_or_exists_not {α : Sort u_2} (P : α → Prop) : (∀ (a : α), P a) ∨ ∃ (a : α), ¬P a

theorem exists_or_forall_not {α : Sort u_2} (P : α → Prop) : (∃ (a : α), P a) ∨ ∀ (a : α), ¬P a

theorem forall_imp_iff_exists_imp {α : Sort u_2} {p : α → Prop} {b : Prop} [ha : Nonempty α] : (∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b

theorem forall_true_iff {α : Sort u_2} : α → True ↔ True

theorem forall_true_iff' {α : Sort u_2} {p : α → Prop} (h : ∀ (a : α), p a ↔ True) : (∀ (a : α), p a) ↔ True

theorem forall₂_true_iff {α : Sort u_3} {β : α → Sort u_2} : (∀ (a : α), β a → True) ↔ True

theorem forall₃_true_iff {α : Sort u_4} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} : (∀ (a : α) (b : β a), γ a b → True) ↔ True

@[simp]

theorem exists_unique_iff_exists {α : Sort u_2} [Subsingleton α] {p : α → Prop} : (∃! (x : α), p x) ↔ ∃ (x : α), p x

theorem exists_unique_const {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α] : (∃! (x : α), b) ↔ b

theorem Decidable.and_forall_ne {α : Sort u_2} [DecidableEq α] (a : α) {p : α → Prop} : (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

theorem and_forall_ne {α : Sort u_2} {p : α → Prop} (a : α) : (p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b

theorem Ne.ne_or_ne {α : Sort u_2} {x : α} {y : α} (z : α) (h : x ≠ y) : x ≠ z ∨ y ≠ z

@[simp]

theorem exists_unique_eq {α : Sort u_2} {a' : α} : ∃! (a : α), a = a'

@[simp]

theorem exists_unique_eq' {α : Sort u_2} {a' : α} : ∃! (a : α), a' = a

theorem exists_apply_eq_apply' {α : Sort u_3} {β : Sort u_2} (f : α → β) (a' : α) : ∃ (a : α), f a' = f a

theorem exists_apply_eq {α : Sort u_3} {β : Sort u_2} (a : α) (b : β) : ∃ (f : α → β), f a = b

@[simp]

theorem exists_exists_and_eq_and {α : Sort u_3} {β : Sort u_2} {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_3} {β : Sort u_2} {f : α → β} {p : β → Prop} : (∃ (b : β), (∃ (a : α), f a = b) ∧ p b) ↔ ∃ (a : α), p (f a)

@[simp]

theorem exists_exists_and_exists_and_eq_and {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {p : α → Prop} {q : β → Prop} {r : γ → Prop} : (∃ (c : γ), (∃ (a : α), p a ∧ ∃ (b : β), q b ∧ f a b = c) ∧ r c) ↔ ∃ (a : α), p a ∧ ∃ (b : β), q b ∧ r (f a b)

@[simp]

theorem exists_or_eq_left {α : Sort u_2} (y : α) (p : α → Prop) : ∃ (x : α), x = y ∨ p x

@[simp]

theorem exists_or_eq_right {α : Sort u_2} (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ x = y

@[simp]

theorem exists_or_eq_left' {α : Sort u_2} (y : α) (p : α → Prop) : ∃ (x : α), y = x ∨ p x

@[simp]

theorem exists_or_eq_right' {α : Sort u_2} (y : α) (p : α → Prop) : ∃ (x : α), p x ∨ y = x

theorem forall_apply_eq_imp_iff' {α : Sort u_3} {β : Sort u_2} {f : α → β} {p : β → Prop} : (∀ (a : α) (b : β), f a = b → p b) ↔ ∀ (a : α), p (f a)

theorem forall_eq_apply_imp_iff' {α : Sort u_3} {β : Sort u_2} {f : α → β} {p : β → Prop} : (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)

@[simp]

theorem exists_eq_right' {α : Sort u_2} {p : α → Prop} {a' : α} : (∃ (a : α), p a ∧ a' = a) ↔ p a'

theorem exists₂_comm {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁ → Sort u_2} {κ₂ : ι₂ → Sort u_3} {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 : Prop} {q : Prop} {f : p ∧ q → Prop} : (∃ (h : p ∧ q), f h) ↔ ∃ (hp : p), ∃ (hq : q), f (_ : p ∧ q)

theorem forall_or_of_or_forall {α : Sort u_2} {p : α → Prop} {b : Prop} (h : b ∨ ∀ (x : α), p x) (x : α) : b ∨ p x

theorem Decidable.forall_or_left {α : Sort u_2} {q : Prop} {p : α → Prop} [Decidable q] : (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

theorem forall_or_left {α : Sort u_2} {q : Prop} {p : α → Prop} : (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

theorem Decidable.forall_or_right {α : Sort u_2} {q : Prop} {p : α → Prop} [Decidable q] : (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

theorem forall_or_right {α : Sort u_2} {q : Prop} {p : α → Prop} : (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

theorem exists_unique_prop {p : Prop} {q : Prop} : (∃! (x : p), q) ↔ p ∧ q

@[simp]

theorem exists_unique_false {α : Sort u_2} : ¬∃! (x : α), False

theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b

theorem Exists.snd {b : Prop} {p : b → Prop} (h : Exists p) : p (_ : b)

theorem Prop.exists_iff {p : Prop → Prop} : (∃ (h : Prop), p h) ↔ p False ∨ p True

theorem Prop.forall_iff {p : Prop → Prop} : (∀ (h : Prop), p h) ↔ p False ∧ p True

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 exists_prop_of_false {p : Prop} {q : p → Prop} : ¬p → ¬∃ (h' : p), q h'

theorem exists_prop_congr {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') : Exists q ↔ ∃ (h : p'), q' (_ : p)

theorem exists_prop_congr' {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') : Exists q = ∃ (h : p'), q' (_ : p)

@[simp]

theorem exists_true_left (p : True → Prop) : (∃ (x : True), p x) ↔ p True.intro

See IsEmpty.exists_iff for the False version.

theorem forall_prop_congr {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') : (∀ (h : p), q h) ↔ ∀ (h : p'), q' (_ : p)

theorem forall_prop_congr' {p : Prop} {p' : Prop} {q : p → Prop} {q' : p → Prop} (hq : ∀ (h : p), q h ↔ q' h) (hp : p ↔ p') : (∀ (h : p), q h) = ∀ (h : p'), q' (_ : p)

@[simp]

theorem forall_true_left (p : True → Prop) : (∀ (x : True), p x) ↔ p True.intro

See IsEmpty.forall_iff for the False version.

theorem ExistsUnique.elim₂ {α : Sort u_2} {p : α → Sort u_3} [∀ (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 ExistsUnique.intro₂ {α : Sort u_2} {p : α → Sort u_3} [∀ (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 ExistsUnique.exists₂ {α : Sort u_2} {p : α → Sort u_3} {q : (x : α) → p x → Prop} (h : ∃! (x : α), ∃! (hx : p x), q x hx) : ∃ (x : α), ∃ (hx : p x), q x hx

theorem ExistsUnique.unique₂ {α : Sort u_2} {p : α → Sort u_3} [∀ (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

noncomputable def Classical.dec (p : Prop) : Decidable p

Any prop p is decidable classically. A shorthand for Classical.propDecidable.

Equations

• Classical.dec p = inferInstance

noncomputable def Classical.decPred {α : Sort u_1} (p : α → Prop) : DecidablePred p

Any predicate p is decidable classically.

Equations

• Classical.decPred p = inferInstance

noncomputable def Classical.decRel {α : Sort u_1} (p : α → α → Prop) : DecidableRel p

Any relation p is decidable classically.

Equations

• Classical.decRel p = inferInstance

noncomputable def Classical.decEq (α : Sort u) : DecidableEq α

Any type α has decidable equality classically.

Equations

• Classical.decEq α = inferInstance

noncomputable def Classical.existsCases {α : Prop} {p : α → Prop} {C : Sort u_1} (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

• Classical.existsCases H0 H = if h : ∃ (a : α), p a then H (_ : α) (_ : p (_ : α)) else H0

theorem Classical.some_spec₂ {α : Sort u_1} {p : α → Prop} {h : ∃ (a : α), p a} (q : α → Prop) (hpq : ∀ (a : α), p a → q a) : q (Classical.choose h)

noncomputable def Classical.subtype_of_exists {α : Type u_1} {P : α → Prop} (h : ∃ (x : α), P x) : { x : α // P x }

A version of Classical.indefiniteDescription which is definitionally equal to a pair

Equations

• Classical.subtype_of_exists h = { val := Classical.choose h, property := (_ : P (Classical.choose h)) }

noncomputable def Classical.byContradiction' {α : Sort u_1} (H : ¬(α → False)) : α

A version of byContradiction that uses types instead of propositions.

Equations

• Classical.byContradiction' H = Classical.choice (_ : Nonempty α)

def Classical.choice_of_byContradiction' {α : Sort u_1} (contra : ¬(α → False) → α) : Nonempty α → α

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

Equations

• Classical.choice_of_byContradiction' contra H = contra (_ : (α → False) → False)

noncomputable def Exists.classicalRecOn {α : Sort u_1} {p : α → Prop} (h : ∃ (a : α), p a) {C : Sort u_2} (H : (a : α) → p a → C) : C

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

Equations

• Exists.classicalRecOn h H = H (Classical.choose h) (_ : p (Classical.choose h))

Declarations about bounded quantifiers

theorem bex_def {α : Sort u_1} {p : α → Prop} {q : α → Prop} : (∃ (x : α), ∃ (x_1 : 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 : (x : α) → p x → Prop} {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 : (x : α) → p x → Prop} {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_1 : x = a), p x) ↔ p a

theorem BAll.imp_right {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} {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 : (x : α) → p x → Prop} {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 : α → Prop} {p : α → Prop} {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 : α → Prop} {p : α → Prop} {q : α → Prop} (H : ∀ (x : α), p x → q x) : (∃ (x : α), ∃ (x_1 : p x), r x) → ∃ (x : α), ∃ (x_1 : 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 : α → Prop} {q : α → Prop} (H : ∀ (x : α), p x) (h : ∀ (x : α), p x → q x) (x : α) : q x

theorem bex_of_exists {α : Sort u_1} {p : α → Prop} {q : α → Prop} (H : ∀ (x : α), p x) : (∃ (x : α), q x) → ∃ (x : α), ∃ (x_1 : p x), q x

theorem exists_of_bex {α : Sort u_1} {p : α → Prop} {q : α → Prop} : (∃ (x : α), ∃ (x_1 : p x), q x) → ∃ (x : α), q x

theorem bex_imp {α : 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

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 {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} {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 {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop} {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 {α : Sort u_1} {r : α → Prop} {p : α → Prop} {q : α → Prop} : (∀ (x : α), p x ∨ q x → r x) ↔ (∀ (x : α), p x → r x) ∧ ∀ (x : α), q x → r x

theorem bex_or_left {α : Sort u_1} {r : α → Prop} {p : α → Prop} {q : α → Prop} : (∃ (x : α), ∃ (x_1 : p x ∨ q x), r x) ↔ (∃ (x : α), ∃ (x_1 : p x), r x) ∨ ∃ (x : α), ∃ (x_1 : q x), r x

theorem dite_eq_iff {α : Sort u_2} {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_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} : (if P then a else b) = c ↔ P ∧ a = c ∨ ¬P ∧ b = c

theorem eq_ite_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} : (a = if P then b else c) ↔ P ∧ a = b ∨ ¬P ∧ a = c

theorem dite_eq_iff' {α : Sort u_2} {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_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} : (if P then a else b) = c ↔ (P → a = c) ∧ (¬P → b = c)

theorem dite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} : dite P (fun (x : P) => a) B ≠ a ↔ ∃ (h : ¬P), a ≠ B h

theorem dite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : P → α} : (dite P A fun (x : ¬P) => b) ≠ b ↔ ∃ (h : P), A h ≠ b

theorem ite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} : (if P then a else b) ≠ a ↔ ¬P ∧ a ≠ b

theorem ite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} : (if P then a else b) ≠ b ↔ P ∧ a ≠ b

theorem Ne.dite_eq_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} (h : ∀ (h : ¬P), a ≠ B h) : dite P (fun (x : P) => a) B = a ↔ P

theorem Ne.dite_eq_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : P → α} (h : ∀ (h : P), A h ≠ b) : (dite P A fun (x : ¬P) => b) = b ↔ ¬P

theorem Ne.ite_eq_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a ≠ b) : (if P then a else b) = a ↔ P

theorem Ne.ite_eq_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a ≠ b) : (if P then a else b) = b ↔ ¬P

theorem Ne.dite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} (h : ∀ (h : ¬P), a ≠ B h) : dite P (fun (x : P) => a) B ≠ a ↔ ¬P

theorem Ne.dite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : P → α} (h : ∀ (h : P), A h ≠ b) : (dite P A fun (x : ¬P) => b) ≠ b ↔ P

theorem Ne.ite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a ≠ b) : (if P then a else b) ≠ a ↔ ¬P

theorem Ne.ite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a ≠ b) : (if P then a else b) ≠ b ↔ P

theorem dite_eq_or_eq {α : Sort u_2} (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_2} (P : Prop) [Decidable P] (a : α) (b : α) : (if P then a else b) = a ∨ (if P then a else b) = b

theorem apply_dite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_2} (f : α → β → γ) (P : Prop) [Decidable P] (a : P → α) (b : ¬P → α) (c : P → β) (d : ¬P → β) : f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else 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.

theorem apply_ite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_2} (f : α → β → γ) (P : Prop) [Decidable P] (a : α) (b : α) (c : β) (d : β) : f (if P then a else b) (if P then c else d) = if P then f a c else 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.

theorem dite_apply {α : Sort u_2} {σ : α → Sort u_1} (P : Prop) [Decidable P] (f : P → (a : α) → σ a) (g : ¬P → (a : α) → σ a) (a : α) : dite P f g a = if h : P then f h a else 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_2} {σ : α → Sort u_1} (P : Prop) [Decidable P] (f : (a : α) → σ a) (g : (a : α) → σ a) (a : α) : ite P f g a = if P then f a else g a

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

theorem ite_and {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) : (if P ∧ Q then a else b) = if P then if Q then a else b else b

theorem dite_dite_comm {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] {A : P → α} {B : Q → α} {C : ¬P → ¬Q → α} (h : P → ¬Q) : (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q

theorem ite_ite_comm {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) {c : α} (h : P → ¬Q) : (if P then a else if Q then b else c) = if Q then b else if P then a else c

theorem ite_prop_iff_or (P : Prop) (Q : Prop) [Decidable P] {R : Prop} : (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

theorem dite_prop_iff_or (P : Prop) {Q : P → Prop} {R : ¬P → Prop} [Decidable P] : dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p

theorem ite_prop_iff_and (P : Prop) (Q : Prop) [Decidable P] {R : Prop} : (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

theorem dite_prop_iff_and (P : Prop) {Q : P → Prop} {R : ¬P → Prop} [Decidable P] : dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h