# 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`.

source
@[reducible, inline]
abbrev 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

Instances For

source
@[instance 10]
instance decidableEq_of_subsingleton {α : Sort u_1} [Subsingleton α] :
DecidableEq α
Equations

- decidableEq_of_subsingleton a b = isTrue ⋯

source
instance instSubsingletonSubtype_mathlib {α : Sort u_1} [Subsingleton α] (p : α → Prop) :
Subsingleton (Subtype p)
source
theorem congr_heq {α β : Sort u_2} {γ : Sort u_3} {f : α → γ} {g : β → γ} {x : α} {y : β} (h₁ : f ≍ g) (h₂ : x ≍ y) :
f x = g y
source
theorem congr_arg_heq {α : Sort u_1} {β : α → Sort u_2} (f : (a : α) → β a) {a₁ a₂ : α} :
a₁ = a₂ → f a₁ ≍ f a₂
source
theorem dcongr_heq {α₁ α₂ : Sort u} {β₁ : α₁ → Sort v} {β₂ : α₂ → Sort v} {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a} {a₁ : α₁} {a₂ : α₂} (hargs : a₁ ≍ a₂) (ht : ∀ (t₁ : α₁) (t₂ : α₂), t₁ ≍ t₂ → β₁ t₁ = β₂ t₂) (hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂) :
f₁ a₁ ≍ f₂ a₂
source
@[simp]
theorem eq_iff_eq_cancel_left {α : Sort u_1} {b c : α} :
(∀ {a : α}, a = b ↔ a = c) ↔ b = c
source
@[simp]
theorem eq_iff_eq_cancel_right {α : Sort u_1} {a b : α} :
(∀ {c : α}, a = c ↔ b = c) ↔ a = b
source
theorem ne_and_eq_iff_right {α : Sort u_1} {a b c : α} (h : b ≠ c) :
a ≠ b ∧ a = c ↔ a = c
source
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`.

Instances

source
def Mathlib.LibraryNote.«fact non-instances» :
LibraryNote

In most cases, we should not have global instances of `Fact`; typeclass search is not an advanced proof search engine, and adding any such instance has the potential to cause slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.

Equations

- Mathlib.LibraryNote.«fact non-instances» = ()

Instances For

source
theorem Fact.elim {p : Prop} (h : Fact p) :
p
source
theorem fact_iff {p : Prop} :
Fact p ↔ p
source
instance instDecidableFact {p : Prop} [Decidable p] :
Decidable (Fact p)
Equations

- instDecidableFact = decidable_of_iff p ⋯

source
@[reducible, inline]
abbrev Function.swap₂ {ι₁ : Sort u_2} {ι₂ : Sort u_3} {κ₁ : ι₁ → Sort u_4} {κ₂ : ι₂ → Sort u_5} {φ : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Sort u_6} (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₂

Instances For

### Declarations about propositional connectives #

### Declarations about `implies` #

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

Alias of `imp_congr`.

source
theorem imp_iff_right_iff {a b : Prop} :
(a → b ↔ b) ↔ a ∨ b
source
theorem and_or_imp {a b c : Prop} :
a ∧ b ∨ (a → c) ↔ a → b ∨ c
source
theorem Function.mt {a b : Prop} :
(a → b) → ¬b → ¬a

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

### Declarations about `not` #

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

Alias of `Decidable.em`.

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

Alias of `Classical.em`.

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

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_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) :
q
source
theorem by_contra {p : Prop} :
(¬p → False) → p

Alias of `by_contradiction`.

source
def Mathlib.LibraryNote.«decidable namespace» :
LibraryNote

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.

Equations

- Mathlib.LibraryNote.«decidable namespace» = ()

Instances For

source
def Mathlib.LibraryNote.«decidable arguments» :
LibraryNote

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.

Equations

- Mathlib.LibraryNote.«decidable arguments» = ()

Instances For

source
theorem of_not_not {a : Prop} :
¬¬a → a
source
theorem not_ne_iff {α : Sort u_1} {a b : α} :
¬a ≠ b ↔ a = b
source
theorem of_not_imp {a b : Prop} :
¬(a → b) → a
source
theorem Not.decidable_imp_symm {a b : Prop} [Decidable a] (h : ¬a → b) (hb : ¬b) :
a

Alias of `Decidable.not_imp_symm`.

source
theorem Not.imp_symm {a b : Prop} :
(¬a → b) → ¬b → a
source
theorem not_imp_comm {a b : Prop} :
¬a → b ↔ ¬b → a
source
@[simp]
theorem not_imp_self {a : Prop} :
¬a → a ↔ a
source
theorem Imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} :
(∀ (a : a) (a : b), c) ↔ ∀ (a_1 : b) (a : a), c
source
theorem Iff.not {a b : Prop} (h : a ↔ b) :
¬a ↔ ¬b

Alias of `not_congr`.

source
theorem Iff.not_left {a b : Prop} (h : a ↔ ¬b) :
¬a ↔ b
source
theorem Iff.not_right {a b : Prop} (h : ¬a ↔ b) :
a ↔ ¬b
source
theorem Iff.ne {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β} :
(a = b ↔ c = d) → (a ≠ b ↔ c ≠ d)
source
theorem Iff.ne_left {α : Sort u_1} {β : Sort u_2} {a b : α} {c d : β} :
(a = b ↔ c ≠ d) → (a ≠ b ↔ c = d)
source
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'` #

source
def Xor' (a b : Prop) :
Prop

`Xor' a b` is the exclusive-or of propositions.

Equations

- Xor' a b = (a ∧ ¬b ∨ b ∧ ¬a)

Instances For

source
theorem xor_def {a b : Prop} :
Xor' a b ↔ a ∧ ¬b ∨ b ∧ ¬a
source
instance instDecidableXor' {a b : Prop} [Decidable a] [Decidable b] :
Decidable (Xor' a b)
Equations

- instDecidableXor' = inferInstanceAs (Decidable (a ∧ ¬b ∨ b ∧ ¬a))

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
instance instCommutativeXor' :
Std.Commutative Xor'
source
@[simp]
theorem xor_self (a : Prop) :
Xor' a a = False
source
@[simp]
theorem xor_not_left {a b : Prop} :
Xor' (¬a) b ↔ (a ↔ b)
source
@[simp]
theorem xor_not_right {a b : Prop} :
Xor' a ¬b ↔ (a ↔ b)
source
theorem xor_not_not {a b : Prop} :
Xor' (¬a) ¬b ↔ Xor' a b
source
theorem Xor'.or {a b : Prop} (h : Xor' a b) :
a ∨ b

### Declarations about `and` #

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

Alias of `and_congr`.

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

Alias of the forward direction of `and_rotate`.

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

### Declarations about `or` #

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

Alias of `or_congr`.

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

Alias of the forward direction of `or_rotate`.

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.imp3 {a b d e c f : Prop} (had : a → d) (hbe : b → e) (hcf : c → f) :
a ∨ b ∨ c → d ∨ e ∨ f
source
theorem not_or_of_imp {a b : Prop} :
(a → b) → ¬a ∨ b
source
theorem Decidable.or_not_of_imp {a b : Prop} [Decidable a] (h : a → b) :
b ∨ ¬a
source
theorem or_not_of_imp {a b : Prop} :
(a → b) → b ∨ ¬a
source
theorem imp_iff_not_or {a b : Prop} :
a → b ↔ ¬a ∨ b
source
theorem imp_iff_or_not {b a : Prop} :
b → a ↔ a ∨ ¬b
source
theorem not_imp_not {a b : Prop} :
¬a → ¬b ↔ b → a
source
theorem imp_and_neg_imp_iff (p q : Prop) :
(p → q) ∧ (¬p → q) ↔ q
source
theorem Function.mtr {a b : Prop} :
(¬a → ¬b) → b → a

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

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

### Declarations about distributivity #

Declarations about `iff`

source
theorem Iff.iff {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) :
(p₁ ↔ q₁) ↔ (p₂ ↔ q₂)

Alias of `iff_congr`.

source
theorem iff_mpr_iff_true_intro {P : Prop} (h : P) :
⋯ = h
source
theorem imp_or {a b c : Prop} :
a → b ∨ c ↔ (a → b) ∨ (a → c)
source
theorem imp_or' {a : Sort u_1} {b c : Prop} :
(∀ (a : a), b ∨ c) ↔ (∀ (a : a), b) ∨ ∀ (a : a), c
source
theorem not_imp {a b : Prop} :
¬(a → b) ↔ a ∧ ¬b
source
theorem peirce (a b : Prop) :
((a → b) → a) → a
source
theorem not_iff_not {a b : Prop} :
(¬a ↔ ¬b) ↔ (a ↔ b)
source
theorem not_iff_comm {a b : Prop} :
(¬a ↔ b) ↔ (¬b ↔ a)
source
theorem not_iff {a b : Prop} :
¬(a ↔ b) ↔ (¬a ↔ b)
source
theorem iff_not_comm {a b : Prop} :
(a ↔ ¬b) ↔ (b ↔ ¬a)
source
theorem iff_iff_and_or_not_and_not {a b : Prop} :
(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
theorem not_and_not_right {a b : Prop} :
¬(a ∧ ¬b) ↔ a → b

### De Morgan's laws #

source
theorem not_and_or {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
theorem or_iff_not_and_not {a b : Prop} :
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)
source
theorem xor_iff_iff_not {a b : Prop} :
Xor' a b ↔ (a ↔ ¬b)
source
theorem xor_iff_not_iff' {a b : Prop} :
Xor' a b ↔ (¬a ↔ b)
source
theorem xor_iff_or_and_not_and (a b : Prop) :
Xor' a b ↔ (a ∨ b) ∧ ¬(a ∧ b)

### Declarations about equality #

source
theorem forall_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
source
theorem forall_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
source
theorem ne_of_eq_of_ne {α : Sort u_1} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) :
a ≠ c
source
theorem ne_of_ne_of_eq {α : Sort u_1} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) :
a ≠ c
source
theorem Eq.trans_ne {α : Sort u_1} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) :
a ≠ c

Alias of `ne_of_eq_of_ne`.

source
theorem Ne.trans_eq {α : Sort u_1} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) :
a ≠ c

Alias of `ne_of_ne_of_eq`.

source
theorem eq_equivalence {α : Sort u_1} :
Equivalence Eq
source
theorem congr_refl_left {α : Sort u_1} {β : Sort u_2} (f : α → β) {a b : α} (h : a = b) :
⋯ = ⋯
source
theorem congr_refl_right {α : Sort u_1} {β : Sort u_2} {f g : α → β} (h : f = g) (a : α) :
⋯ = ⋯
source
theorem congr_arg_refl {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α) :
⋯ = ⋯
source
theorem congr_fun_rfl {α : Sort u_1} {β : Sort u_2} (f : α → β) (a : α) :
⋯ = ⋯
source
theorem congr_fun_congr_arg {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {a a' : α} (p : a = a') (b : β) :
⋯ = ⋯
source
@[deprecated eqRec_eq_cast (since := "2025-09-16")]
theorem Eq.rec_eq_cast {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :
e ▸ x = cast ⋯ x

Alias of `eqRec_eq_cast`.

source
@[deprecated eqRec_heq_self (since := "2025-09-16")]
theorem eqRec_heq' {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :
e ▸ x ≍ x

Alias of `eqRec_heq_self`.

source
theorem rec_heq_of_heq {α : Sort u_2} {β : Sort u_1} {a b : α} {C : α → Sort u_1} {x : C a} {y : β} (e : a = b) (h : x ≍ y) :
e ▸ x ≍ y
source
@[deprecated eqRec_heq_iff_heq (since := "2025-09-16")]
theorem rec_heq_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :
e ▸ x ≍ y ↔ x ≍ y

Alias of `eqRec_heq_iff_heq`.

source
@[deprecated heq_eqRec_iff_heq (since := "2025-09-16")]
theorem heq_rec_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :
y ≍ e ▸ x ↔ y ≍ x

Alias of `heq_eqRec_iff_heq`.

source
@[simp]
theorem cast_heq_iff_heq {α β γ : Sort u_1} (e : α = β) (a : α) (c : γ) :
cast e a ≍ c ↔ a ≍ c
source
@[simp]
theorem heq_cast_iff_heq {α β γ : Sort u_1} (e : β = γ) (a : α) (b : β) :
a ≍ cast e b ↔ a ≍ b
source
theorem heq_of_eq_cast {α β : Sort u} {a : α} {b : β} (e : β = α) :
a = cast e b → a ≍ b
source
theorem eq_cast_iff_heq {α β : Sort u} {e : β = α} {a : α} {b : β} :
a = cast e b ↔ a ≍ b
source
theorem heq_iff_exists_eq_cast {α β : Sort u} {a : α} {b : β} :
a ≍ b ↔ ∃ (h : β = α), a = cast h b
source
theorem heq_iff_exists_cast_eq {α β : Sort u} {a : α} {b : β} :
a ≍ b ↔ ∃ (h : α = β), cast h a = b

### Declarations about quantifiers #

source
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
source
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
source
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
source
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
source
theorem forall_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y
source
theorem forall₂_swap {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6} {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₂
source
theorem imp_forall_iff {α : Type u_3} {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 imp_forall_iff_forall (A : Prop) (B : A → Prop) :
(A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
source
theorem exists_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :
(∃ (x : α), ∃ (y : β), p x y) ↔ ∃ (y : β), ∃ (x : α), p x y
source
theorem exists_and_exists_comm {α : Sort u_1} {β : Sort u_2} {P : α → Prop} {Q : β → Prop} :
((∃ (a : α), P a) ∧ ∃ (b : β), Q b) ↔ ∃ (a : α), ∃ (b : β), P a ∧ Q b
source
theorem not_forall_not {α : Sort u_1} {p : α → Prop} :
(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x
source
theorem forall_or_exists_not {α : Sort u_1} (P : α → Prop) :
(∀ (a : α), P a) ∨ ∃ (a : α), ¬P a
source
theorem exists_or_forall_not {α : Sort u_1} (P : α → Prop) :
(∃ (a : α), P a) ∨ ∀ (a : α), ¬P a
source
theorem forall_imp_iff_exists_imp {α : Sort u_3} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
(∀ (x : α), p x) → b ↔ ∃ (x : α), p x → b
source
theorem forall_true_iff {α : Sort u_1} :
(∀ (a : α), True) ↔ True
source
theorem forall_true_iff' {α : Sort u_1} {p : α → Prop} (h : ∀ (a : α), p a ↔ True) :
(∀ (a : α), p a) ↔ True
source
theorem forall₂_true_iff {α : Sort u_1} {β : α → Sort u_3} :
(∀ (a : α) (a : β a), True) ↔ True
source
theorem forall₃_true_iff {α : Sort u_1} {β : α → Sort u_3} {γ : (a : α) → β a → Sort u_4} :
(∀ (a : α) (b : β a) (a : γ a b), True) ↔ True
source
theorem Decidable.and_forall_ne {α : Sort u_1} [DecidableEq α] (a : α) {p : α → Prop} :
(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
source
theorem and_forall_ne {α : Sort u_1} {p : α → Prop} (a : α) :
(p a ∧ ∀ (b : α), b ≠ a → p b) ↔ ∀ (b : α), p b
source
theorem Ne.ne_or_ne {α : Sort u_1} {x y : α} (z : α) (h : x ≠ y) :
x ≠ z ∨ y ≠ z
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_apply2 {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : α → β → γ} {a : α} {b : β} :
∃ (x : α), ∃ (y : β), f x y = f a b
source
@[simp]
theorem exists_apply_eq_apply2' {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {f : α → β → γ} {a : α} {b : β} :
∃ (x : α), ∃ (y : β), f a b = f x y
source
@[simp]
theorem exists_apply_eq_apply3 {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} :
∃ (x : α), ∃ (y : β), ∃ (z : γ), f x y z = f a b c
source
@[simp]
theorem exists_apply_eq_apply3' {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {δ : Sort u_6} {f : α → β → γ → δ} {a : α} {b : β} {c : γ} :
∃ (x : α), ∃ (y : β), ∃ (z : γ), f a b c = f x y z
source
theorem exists_apply_eq {α : Sort u_1} {β : Sort u_2} (a : α) (b : β) :
∃ (f : α → β), f a = b

The constant function witnesses that there exists a function sending a given term to a given term.

This is sometimes useful in `simp` to discharge side conditions.

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_exists_and_exists_and_eq_and {α : Type u_3} {β : Type u_4} {γ : Type u_5} {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)
source
@[simp]
theorem exists_exists_exists_and_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β → γ} {p : γ → Prop} :
(∃ (c : γ), (∃ (a : α), ∃ (b : β), f a b = c) ∧ p c) ↔ ∃ (a : α), ∃ (b : β), p (f a b)
source
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
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
theorem exists₂_comm {ι₁ : Sort u_3} {ι₂ : Sort u_4} {κ₁ : ι₁ → Sort u_5} {κ₂ : ι₂ → Sort u_6} {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₂
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_3} {p : α → Prop} {b : Prop} (h : b ∨ ∀ (x : α), p x) (x : α) :
b ∨ p x
source
theorem Decidable.forall_or_left {α : Sort u_1} {q : Prop} {p : α → Prop} [Decidable q] :
(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
source
theorem forall_or_left {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
source
theorem Decidable.forall_or_right {α : Sort u_1} {q : Prop} {p : α → Prop} [Decidable q] :
(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
source
theorem forall_or_right {α : Sort u_1} {q : Prop} {p : α → Prop} :
(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
source
@[simp]
theorem forall_and_index {p q : Prop} {r : p ∧ q → Prop} :
(∀ (h : p ∧ q), r h) ↔ ∀ (hp : p) (hq : q), r ⋯
source
theorem forall_and_index' {p q : Prop} {r : p → q → Prop} :
(∀ (hp : p) (hq : q), r hp hq) ↔ ∀ (h : p ∧ q), r ⋯ ⋯
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 Prop.exists_iff {p : Prop → Prop} :
(∃ (h : Prop), p h) ↔ p False ∨ p True
source
theorem Prop.forall_iff {p : Prop → Prop} :
(∀ (h : Prop), p h) ↔ p False ∧ p True
source
theorem exists_iff_of_forall {p : Prop} {q : p → Prop} (h : ∀ (h : p), q h) :
(∃ (h : p), q h) ↔ p
source
theorem exists_prop_of_false {p : Prop} {q : p → Prop} :
¬p → ¬∃ (h' : p), q h'
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
theorem imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) :
(a → b) = (c → d)
source
theorem imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → b = d) :
(a → b) = (c → d)
source
theorem eq_true_intro {a : Prop} (h : a) :
a = True
source
theorem eq_false_intro {a : Prop} (h : ¬a) :
a = False
source
def Iff.eq {a b : Prop} :
(a ↔ b) → a = b

Alias of `propext`.

The axiom of propositional extensionality. It asserts that if propositions `a` and `b` are logically equivalent (that is, if `a` can be proved from `b` and vice versa), then `a` and `b` are equal, meaning `a` can be replaced with `b` in all contexts.

The standard logical connectives provably respect propositional extensionality. However, an axiom is needed for higher order expressions like `P a` where `P : Prop → Prop` is unknown, as well as for equality. Propositional extensionality is intuitionistically valid.

Equations

- @Iff.eq = @propext

Instances For

source
theorem iff_eq_eq {a b : Prop} :
(a ↔ b) = (a = b)
source
@[simp]
theorem forall_true_left (p : True → Prop) :
(∀ (x : True), p x) ↔ p True.intro

See `IsEmpty.forall_iff` for the `False` version.

### Classical lemmas #

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

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

Equations

- Classical.dec p = inferInstance

Instances For

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

Any predicate `p` is decidable classically.

Equations

- Classical.decPred p = inferInstance

Instances For

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

Any relation `p` is decidable classically.

Equations

- Classical.decRel p = inferInstance

Instances For

source
noncomputable def Classical.decEq (α : Sort u_2) :
DecidableEq α

Any type `α` has decidable equality classically.

Equations

- Classical.decEq α = inferInstance

Instances For

source
noncomputable def Classical.existsCases {α : Sort u_2} {C : Sort u_3} {p : α → Prop} (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 (Classical.choose h) ⋯ else H0

Instances For

source
theorem Classical.some_spec₂ {α : Sort u_2} {p : α → Prop} {h : ∃ (a : α), p a} (q : α → Prop) (hpq : ∀ (a : α), p a → q a) :
q (choose h)
source
noncomputable def Classical.byContradiction' {α : Sort u_2} (H : ¬∀ (a : α), False) :
α

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

Equations

- Classical.byContradiction' H = Classical.choice ⋯

Instances For

source
def Classical.choice_of_byContradiction' {α : Sort u_2} (contra : (¬∀ (a : α), False) → α) :
Nonempty α → α

`Classical.byContradiction'` is equivalent to lean's axiom `Classical.choice`.

Equations

- Classical.choice_of_byContradiction' contra H = contra ⋯

Instances For

source
@[simp]
theorem Classical.choose_eq {α : Sort u_1} (a : α) :
⋯.choose = a
source
@[simp]
theorem Classical.choose_eq' {α : Sort u_1} (a : α) :
⋯.choose = a
source
theorem Classical.axiom_of_choice {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop} (h : ∀ (x : α), ∃ (y : β x), r x y) :
∃ (f : (x : α) → β x), ∀ (x : α), r x (f x)

Alias of `Classical.axiomOfChoice`.

the axiom of choice

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

Alias of `Classical.byCases`.

source
theorem Classical.by_contradiction {p : Prop} (h : ¬p → False) :
p

Alias of `Classical.byContradiction`.

source
theorem Classical.prop_complete (a : Prop) :
a = True ∨ a = False

Alias of `Classical.propComplete`.

source
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

- h.classicalRecOn H = H (Classical.choose h) ⋯

Instances For

### Declarations about bounded quantifiers #

source
theorem bex_def {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α), ∃ (x_1 : 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.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_1 : p x), r x) → ∃ (x : α), ∃ (x_1 : q x), r x
source
theorem exists_mem_of_exists {α : Sort u_1} {p q : α → Prop} (H : ∀ (x : α), p x) :
(∃ (x : α), q x) → ∃ (x : α), ∃ (x_1 : p x), q x
source
theorem exists_of_exists_mem {α : Sort u_1} {p q : α → Prop} :
(∃ (x : α), ∃ (x_1 : p x), q x) → ∃ (x : α), q x
source
theorem not_exists_mem {α : 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_forall₂_of_exists₂_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
theorem Decidable.not_forall₂ {α : 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_forall₂ {α : 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 forall₂_and {α : 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 forall_and_left {α : Sort u_1} [Nonempty α] (q : Prop) (p : α → Prop) :
(∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x
source
theorem forall_and_right {α : Sort u_1} [Nonempty α] (p : α → Prop) (q : Prop) :
(∀ (x : α), p x ∧ q) ↔ (∀ (x : α), p x) ∧ q
source
theorem exists_mem_or {α : 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 forall₂_or_left {α : 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 exists_mem_or_left {α : Sort u_1} {r p 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
source
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
source
theorem ite_eq_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b c : α} :
(if P then a else b) = c ↔ P ∧ a = c ∨ ¬P ∧ b = c
source
theorem eq_ite_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b c : α} :
(a = if P then b else c) ↔ P ∧ a = b ∨ ¬P ∧ a = c
source
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
source
theorem ite_eq_iff' {α : Sort u_1} {P : Prop} [Decidable P] {a b c : α} :
(if P then a else b) = c ↔ (P → a = c) ∧ (¬P → b = c)
source
theorem dite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} :
dite P (fun (x : P) => a) B ≠ a ↔ ∃ (h : ¬P), a ≠ B h
source
theorem dite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {b : α} {A : P → α} :
(dite P A fun (x : ¬P) => b) ≠ b ↔ ∃ (h : P), A h ≠ b
source
theorem ite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} :
(if P then a else b) ≠ a ↔ ¬P ∧ a ≠ b
source
theorem ite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} :
(if P then a else b) ≠ b ↔ P ∧ a ≠ b
source
theorem Ne.dite_eq_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} (h : ∀ (h : ¬P), a ≠ B h) :
dite P (fun (x : P) => a) B = a ↔ P
source
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 fun (x : ¬P) => b) = b ↔ ¬P
source
theorem Ne.ite_eq_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} (h : a ≠ b) :
(if P then a else b) = a ↔ P
source
theorem Ne.ite_eq_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} (h : a ≠ b) :
(if P then a else b) = b ↔ ¬P
source
theorem Ne.dite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a : α} {B : ¬P → α} (h : ∀ (h : ¬P), a ≠ B h) :
dite P (fun (x : P) => a) B ≠ a ↔ ¬P
source
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 fun (x : ¬P) => b) ≠ b ↔ P
source
theorem Ne.ite_ne_left_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} (h : a ≠ b) :
(if P then a else b) ≠ a ↔ ¬P
source
theorem Ne.ite_ne_right_iff {α : Sort u_1} {P : Prop} [Decidable P] {a b : α} (h : a ≠ b) :
(if P then a else b) ≠ b ↔ P
source
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
source
theorem ite_eq_or_eq {α : Sort u_1} (P : Prop) [Decidable P] (a b : α) :
(if P then a else b) = a ∨ (if P then a else b) = b
source
theorem apply_dite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (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 `dite`s is a `dite` of that two-argument function applied to each of the branches.

source
theorem apply_ite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (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 `ite`s is a `ite` of that two-argument function applied to each of the branches.

source
theorem dite_apply {α : Sort u_1} {σ : α → Sort u_2} (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`.

source
theorem ite_apply {α : Sort u_1} {σ : α → Sort u_2} (P : Prop) [Decidable P] (f g : (a : α) → σ a) (a : α) :
(if P then f else 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`.

source
theorem ite_and {α : Sort u_1} (P Q : Prop) [Decidable P] (a b : α) [Decidable Q] :
(if P ∧ Q then a else b) = if P then if Q then a else b else b
source
theorem ite_or {α : Sort u_1} (P Q : Prop) [Decidable P] (a b : α) [Decidable Q] :
(if P ∨ Q then a else b) = if P then a else if Q then a else b
source
theorem dite_dite_comm {α : Sort u_1} (P Q : Prop) [Decidable P] {A : P → α} [Decidable Q] {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
source
theorem ite_ite_comm {α : Sort u_1} (P Q : Prop) [Decidable P] (a b : α) {c : α} [Decidable Q] (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
source
theorem ite_prop_iff_or {P Q R : Prop} [Decidable P] :
(if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
source
theorem dite_prop_iff_or {P : Prop} [Decidable P] {Q : P → Prop} {R : ¬P → Prop} :
dite P Q R ↔ (∃ (p : P), Q p) ∨ ∃ (p : ¬P), R p
source
theorem ite_prop_iff_and {P Q R : Prop} [Decidable P] :
(if P then Q else R) ↔ (P → Q) ∧ (¬P → R)
source
theorem dite_prop_iff_and {P : Prop} [Decidable P] {Q : P → Prop} {R : ¬P → Prop} :
dite P Q R ↔ (∀ (h : P), Q h) ∧ ∀ (h : ¬P), R h
source
theorem if_ctx_congr {α : Sort u_1} {P Q : Prop} [Decidable P] [Decidable Q] {x y u v : α} (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) :
(if P then x else y) = if Q then u else v
source
theorem if_congr {α : Sort u_1} {P Q : Prop} [Decidable P] [Decidable Q] {x y u v : α} (h_c : P ↔ Q) (h_t : x = u) (h_e : y = v) :
(if P then x else y) = if Q then u else v

### Membership #

source
theorem Membership.mem.ne_of_notMem {α : 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`.

source
theorem Membership.mem.ne_of_notMem' {α : 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'`.

source
@[deprecated Membership.mem.ne_of_notMem (since := "2025-05-23")]
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`.

Alias of `ne_of_mem_of_not_mem`.

source
@[deprecated Membership.mem.ne_of_notMem' (since := "2025-05-23")]
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'`.

Alias of `ne_of_mem_of_not_mem'`.

source
theorem mem_dite {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : α} {s : p → β} {t : ¬p → β} :
(a ∈ if h : p then s h else t h) ↔ (∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h
source
theorem dite_mem {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} {s : β} :
(if h : p then a h else b h) ∈ s ↔ (∀ (h : p), a h ∈ s) ∧ ∀ (h : ¬p), b h ∈ s
source
theorem mem_ite {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a : α} {s t : β} :
(a ∈ if p then s else t) ↔ (p → a ∈ s) ∧ (¬p → a ∈ t)
source
theorem ite_mem {α : Type u_1} {β : Type u_2} [Membership α β] {p : Prop} [Decidable p] {a b : α} {s : β} :
(if p then a else b) ∈ s ↔ (p → a ∈ s) ∧ (¬p → b ∈ s)
source
theorem not_beq_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) :
¬(a == b) = true
source
theorem beq_eq_decide {α : Type u_1} [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
(a == b) = decide (a = b)

Alias of `Bool.beq_eq_decide_eq`.

source
@[simp]
theorem beq_eq_beq {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α} {b₁ b₂ : β} :
(a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)
source
theorem beq_ext {α : Type u_1} (inst1 inst2 : BEq α) (h : ∀ (x y : α), (x == y) = (x == y)) :
inst1 = inst2
source
theorem beq_ext_iff {α : Type u_1} {inst1 inst2 : BEq α} :
inst1 = inst2 ↔ ∀ (x y : α), (x == y) = (x == y)
source
theorem lawful_beq_subsingleton {α : Type u_1} (inst1 inst2 : BEq α) [LawfulBEq α] [LawfulBEq α] :
inst1 = inst2