Module docstring
{"## cast and equality ","## not ","## and ","## or ","## distributivity ","## not equal ","## Ite ","## exists and forall ","## membership ","## Nonempty ","## decidable "}
cast_cast
theorem
: ∀ (ha : α = β) (hb : β = γ) (a : α), cast hb (cast ha a) = cast (ha.trans hb) a
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, given equalities $\alpha = \beta$ and $\beta = \gamma$, and any element $a : \alpha$, the composition of casts along these equalities satisfies $\text{cast}_{hb}(\text{cast}_{ha}(a)) = \text{cast}_{ha \cdot hb}(a)$, where $ha \cdot hb$ denotes the transitivity of the equalities.
not_not_em
theorem
(a : Prop) : ¬¬(a ∨ ¬a)
Full source
theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))Informal description
For any proposition $a$, the double negation of the law of excluded middle holds, i.e., $\neg\neg(a \lor \neg a)$.
and_self_iff
theorem
: a ∧ a ↔ a
Full source
theorem and_self_iff : a ∧ aa ∧ a ↔ a := Iff.of_eq (and_self a)Informal description
For any proposition $a$, the conjunction $a \land a$ is equivalent to $a$, i.e., $a \land a \leftrightarrow a$.
and_not_self_iff
theorem
(a : Prop) : a ∧ ¬a ↔ False
Full source
theorem and_not_self_iff (a : Prop) : a ∧ ¬aa ∧ ¬a ↔ False := iff_false_intro and_not_selfInformal description
For any proposition $a$, the conjunction $a \land \neg a$ is equivalent to $\mathrm{False}$.
not_and_self_iff
theorem
(a : Prop) : ¬a ∧ a ↔ False
Full source
theorem not_and_self_iff (a : Prop) : ¬a¬a ∧ a¬a ∧ a ↔ False := iff_false_intro not_and_selfInformal description
For any proposition $a$, the conjunction of $\neg a$ and $a$ is equivalent to false, i.e., $\neg a \land a \leftrightarrow \text{False}$.
And.imp
theorem
(f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d
Informal description
For any propositions $a, b, c, d$ and functions $f : a \to c$, $g : b \to d$, if $a \land b$ holds, then $c \land d$ holds.
And.imp_left
theorem
(h : a → b) : a ∧ c → b ∧ c
Full source
theorem And.imp_left (h : a → b) : a ∧ c → b ∧ c := .imp h idInformal description
For any propositions $a, b, c$, if $h : a \to b$ is a function, then $a \land c$ implies $b \land c$.
And.imp_right
theorem
(h : a → b) : c ∧ a → c ∧ b
Full source
theorem And.imp_right (h : a → b) : c ∧ a → c ∧ b := .imp id hInformal description
For any propositions $a, b, c$, if $h : a \to b$ is a function, then $c \land a$ implies $c \land b$.
and_congr
theorem
(h₁ : a ↔ c) (h₂ : b ↔ d) : a ∧ b ↔ c ∧ d
Informal description
For any propositions $a, b, c, d$, if $a \leftrightarrow c$ and $b \leftrightarrow d$ hold, then $a \land b$ holds if and only if $c \land d$ holds.
and_congr_left'
theorem
(h : a ↔ b) : a ∧ c ↔ b ∧ c
Full source
theorem and_congr_left' (h : a ↔ b) : a ∧ ca ∧ c ↔ b ∧ c := and_congr h .rflInformal description
For any propositions $a, b, c$, if $a \leftrightarrow b$ holds, then $a \land c$ holds if and only if $b \land c$ holds.
and_congr_right'
theorem
(h : b ↔ c) : a ∧ b ↔ a ∧ c
Full source
theorem and_congr_right' (h : b ↔ c) : a ∧ ba ∧ b ↔ a ∧ c := and_congr .rfl hInformal description
For any propositions $a, b, c$, if $b \leftrightarrow c$ holds, then $a \land b$ holds if and only if $a \land c$ holds.
not_and_of_not_left
theorem
(b : Prop) : ¬a → ¬(a ∧ b)
Full source
theorem not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) := mt And.leftInformal description
For any proposition $b$, if $\neg a$ holds, then $\neg (a \land b)$ holds.
not_and_of_not_right
theorem
(a : Prop) {b : Prop} : ¬b → ¬(a ∧ b)
Full source
theorem not_and_of_not_right (a : Prop) {b : Prop} : ¬b → ¬(a ∧ b) := mt And.rightInformal description
For any propositions $a$ and $b$, if $b$ is false (i.e., $\neg b$ holds), then the conjunction $a \land b$ is also false (i.e., $\neg(a \land b)$ holds).
and_congr_right_eq
theorem
(h : a → b = c) : (a ∧ b) = (a ∧ c)
Full source
theorem and_congr_right_eq (h : a → b = c) : (a ∧ b) = (a ∧ c) :=
propext (and_congr_right (Iff.of_eqIff.of_eq ∘ h))Informal description
For any propositions $a$, $b$, and $c$, if $a$ implies that $b$ is equal to $c$ (i.e., $a \to b = c$), then the conjunction $a \land b$ is equal to $a \land c$.
and_congr_left_eq
theorem
(h : c → a = b) : (a ∧ c) = (b ∧ c)
Full source
theorem and_congr_left_eq (h : c → a = b) : (a ∧ c) = (b ∧ c) :=
propext (and_congr_left (Iff.of_eqIff.of_eq ∘ h))Informal description
For any propositions $a$, $b$, and $c$, if $c$ implies that $a$ is equal to $b$ (i.e., $c \to a = b$), then the conjunction $a \land c$ is equal to $b \land c$.
and_left_comm
theorem
: a ∧ b ∧ c ↔ b ∧ a ∧ c
Full source
theorem and_left_comm : a ∧ b ∧ ca ∧ b ∧ c ↔ b ∧ a ∧ c :=
Iff.intro (fun ⟨ha, hb, hc⟩ => ⟨hb, ha, hc⟩)
(fun ⟨hb, ha, hc⟩ => ⟨ha, hb, hc⟩)Informal description
For any propositions $a$, $b$, and $c$, the conjunction $a \land b \land c$ is equivalent to $b \land a \land c$.
and_right_comm
theorem
: (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b
Full source
theorem and_right_comm : (a ∧ b) ∧ c(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
Iff.intro (fun ⟨⟨ha, hb⟩, hc⟩ => ⟨⟨ha, hc⟩, hb⟩)
(fun ⟨⟨ha, hc⟩, hb⟩ => ⟨⟨ha, hb⟩, hc⟩)Informal description
For any propositions $a$, $b$, and $c$, the conjunction $(a \land b) \land c$ is equivalent to $(a \land c) \land b$.
and_rotate
theorem
: a ∧ b ∧ c ↔ b ∧ c ∧ a
Full source
theorem and_rotate : a ∧ b ∧ ca ∧ b ∧ c ↔ b ∧ c ∧ a := by rw [and_left_comm, @and_comm a c]Informal description
For any propositions $a$, $b$, and $c$, the conjunction $a \land b \land c$ is equivalent to $b \land c \land a$.
and_and_and_comm
theorem
: (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d
Full source
theorem and_and_and_comm : (a ∧ b) ∧ c ∧ d(a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d := by rw [← and_assoc, @and_right_comm a, and_assoc]Informal description
For any propositions $a$, $b$, $c$, and $d$, the conjunction $(a \land b) \land c \land d$ is equivalent to $(a \land c) \land b \land d$.
and_and_left
theorem
: a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c
Full source
theorem and_and_left : a ∧ (b ∧ c)a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c := by rw [and_and_and_comm, and_self]Informal description
For any propositions $a$, $b$, and $c$, the conjunction $a \land (b \land c)$ is equivalent to $(a \land b) \land a \land c$.
and_and_right
theorem
: (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c
Full source
theorem and_and_right : (a ∧ b) ∧ c(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c := by rw [and_and_and_comm, and_self]Informal description
For any propositions $a$, $b$, and $c$, the conjunction $(a \land b) \land c$ is equivalent to $(a \land c) \land b \land c$.
and_iff_left
theorem
(hb : b) : a ∧ b ↔ a
Informal description
For any propositions $a$ and $b$, if $b$ holds, then $a \land b$ is equivalent to $a$.
and_iff_right
theorem
(ha : a) : a ∧ b ↔ b
Informal description
For any propositions $a$ and $b$, if $a$ holds, then the conjunction $a \land b$ is equivalent to $b$.
or_self_iff
theorem
: a ∨ a ↔ a
Full source
theorem or_self_iff : a ∨ aa ∨ a ↔ a := or_self _ ▸ .rflInformal description
For any proposition $a$, the disjunction $a \lor a$ is equivalent to $a$, i.e., $a \lor a \leftrightarrow a$.
not_or_intro
theorem
{a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b)
Full source
theorem not_or_intro {a b : Prop} (ha : ¬a) (hb : ¬b) : ¬(a ∨ b) := (·.elim ha hb)Informal description
For any propositions $a$ and $b$, if $\neg a$ and $\neg b$ hold, then $\neg (a \lor b)$ holds.
or_congr
theorem
(h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d)
Full source
theorem or_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := ⟨.imp h₁.mp h₂.mp, .imp h₁.mpr h₂.mpr⟩Informal description
For any propositions $a$, $b$, $c$, and $d$, if $a$ is equivalent to $c$ and $b$ is equivalent to $d$, then the disjunction $a \lor b$ is equivalent to the disjunction $c \lor d$.
or_congr_left
theorem
(h : a ↔ b) : a ∨ c ↔ b ∨ c
Full source
theorem or_congr_left (h : a ↔ b) : a ∨ ca ∨ c ↔ b ∨ c := or_congr h .rflInformal description
For any propositions $a$, $b$, and $c$, if $a$ is equivalent to $b$, then the disjunction $a \lor c$ is equivalent to $b \lor c$.
or_congr_right
theorem
(h : b ↔ c) : a ∨ b ↔ a ∨ c
Full source
theorem or_congr_right (h : b ↔ c) : a ∨ ba ∨ b ↔ a ∨ c := or_congr .rfl hInformal description
For any propositions $a$, $b$, and $c$, if $b$ is equivalent to $c$, then the disjunction $a \lor b$ is equivalent to $a \lor c$.
or_left_comm
theorem
: a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)
Full source
theorem or_left_comm : a ∨ (b ∨ c)a ∨ (b ∨ c) ↔ b ∨ (a ∨ c) := by rw [← or_assoc, ← or_assoc, @or_comm a b]Informal description
For any propositions $a$, $b$, and $c$, the statement $a ∨ (b ∨ c)$ is logically equivalent to $b ∨ (a ∨ c)$.
or_right_comm
theorem
: (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b
Full source
theorem or_right_comm : (a ∨ b) ∨ c(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc, or_assoc, @or_comm b]Informal description
For any propositions $a$, $b$, and $c$, the disjunction $(a \lor b) \lor c$ is equivalent to $(a \lor c) \lor b$.
or_or_or_comm
theorem
: (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d
Full source
theorem or_or_or_comm : (a ∨ b) ∨ c ∨ d(a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d := by rw [← or_assoc, @or_right_comm a, or_assoc]Informal description
For any propositions $a$, $b$, $c$, and $d$, the disjunction $(a \lor b) \lor c \lor d$ is equivalent to $(a \lor c) \lor b \lor d$.
or_or_distrib_left
theorem
: a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c
Full source
theorem or_or_distrib_left : a ∨ b ∨ ca ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c := by rw [or_or_or_comm, or_self]Informal description
For any propositions $a$, $b$, and $c$, the disjunction $a \lor b \lor c$ is equivalent to $(a \lor b) \lor a \lor c$.
or_or_distrib_right
theorem
: (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c
Full source
theorem or_or_distrib_right : (a ∨ b) ∨ c(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b ∨ c := by rw [or_or_or_comm, or_self]Informal description
For any propositions $a$, $b$, and $c$, the disjunction $(a \lor b) \lor c$ is equivalent to $(a \lor c) \lor b \lor c$.
or_rotate
theorem
: a ∨ b ∨ c ↔ b ∨ c ∨ a
Full source
theorem or_rotate : a ∨ b ∨ ca ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_comm, Or.comm]Informal description
For any propositions $a$, $b$, and $c$, the disjunction $a ∨ b ∨ c$ is equivalent to $b ∨ c ∨ a$.
or_iff_left
theorem
(hb : ¬b) : a ∨ b ↔ a
Full source
theorem or_iff_left (hb : ¬b) : a ∨ ba ∨ b ↔ a := or_iff_left_iff_imp.mpr hb.elimInformal description
For any propositions $a$ and $b$, if $b$ is false ($\neg b$ holds), then the disjunction $a \lor b$ is equivalent to $a$.
or_iff_right
theorem
(ha : ¬a) : a ∨ b ↔ b
Full source
theorem or_iff_right (ha : ¬a) : a ∨ ba ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elimInformal description
For any propositions $a$ and $b$, if $\neg a$ holds, then the disjunction $a \lor b$ is equivalent to $b$.
not_imp_of_and_not
theorem
: a ∧ ¬b → ¬(a → b)
Full source
theorem not_imp_of_and_not : a ∧ ¬b → ¬(a → b)
| ⟨ha, hb⟩, h => hb <| h haInformal description
If $a$ holds and $b$ does not hold, then the implication $a \to b$ does not hold. In other words, $(a \land \neg b) \to \neg(a \to b)$.
imp_and
theorem
{α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c)
Full source
theorem imp_and {α} : (α → b ∧ c) ↔ (α → b) ∧ (α → c) :=
⟨fun h => ⟨fun ha => (h ha).1, fun ha => (h ha).2⟩, fun h ha => ⟨h.1 ha, h.2 ha⟩⟩Informal description
For any proposition $\alpha$ and statements $b$ and $c$, the implication $\alpha \to (b \land c)$ holds if and only if both implications $\alpha \to b$ and $\alpha \to c$ hold. In other words, $\alpha$ implies the conjunction of $b$ and $c$ if and only if $\alpha$ implies $b$ and $\alpha$ implies $c$ separately.
not_and'
theorem
: ¬(a ∧ b) ↔ b → ¬a
Full source
theorem not_and' : ¬(a ∧ b)¬(a ∧ b) ↔ b → ¬a := Iff.trans not_and imp_not_commInformal description
The negation of the conjunction of two propositions $a$ and $b$ is equivalent to the implication that if $b$ holds, then $a$ does not hold. In symbols:
\[
\neg(a \land b) \leftrightarrow (b \to \neg a)
\]
and_or_left
theorem
: a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c)
Full source
/-- `∧` distributes over `∨` (on the left). -/
theorem and_or_left : a ∧ (b ∨ c)a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) :=
Iff.intro (fun ⟨ha, hbc⟩ => hbc.imp (.intro ha) (.intro ha))
(Or.rec (.imp_right .inl) (.imp_right .inr))Informal description
For any propositions $a$, $b$, and $c$, the conjunction of $a$ with the disjunction $b \lor c$ is equivalent to the disjunction of the conjunctions $a \land b$ and $a \land c$. In symbols:
\[
a \land (b \lor c) \leftrightarrow (a \land b) \lor (a \land c)
\]
or_and_right
theorem
: (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c)
Full source
/-- `∧` distributes over `∨` (on the right). -/
theorem or_and_right : (a ∨ b) ∧ c(a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := by rw [@and_comm (a ∨ b), and_or_left, @and_comm c, @and_comm c]Informal description
For any propositions $a$, $b$, and $c$, the conjunction of the disjunction $a \lor b$ with $c$ is equivalent to the disjunction of the conjunctions $a \land c$ and $b \land c$. In symbols:
\[
(a \lor b) \land c \leftrightarrow (a \land c) \lor (b \land c)
\]
or_and_left
theorem
: a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c)
Full source
/-- `∨` distributes over `∧` (on the left). -/
theorem or_and_left : a ∨ (b ∧ c)a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) :=
Iff.intro (Or.rec (fun ha => ⟨.inl ha, .inl ha⟩) (.imp .inr .inr))
(And.rec <| .rec (fun _ => .inl ·) (.imp_right.imp_right ∘ .intro))Informal description
For any propositions $a$, $b$, and $c$, the disjunction $a \lor (b \land c)$ holds if and only if both $(a \lor b) \land (a \lor c)$ hold.
and_or_right
theorem
: (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c)
Full source
/-- `∨` distributes over `∧` (on the right). -/
theorem and_or_right : (a ∧ b) ∨ c(a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := by rw [@or_comm (a ∧ b), or_and_left, @or_comm c, @or_comm c]Informal description
For any propositions $a$, $b$, and $c$, the disjunction $(a \land b) \lor c$ holds if and only if both $(a \lor c) \land (b \lor c)$ hold.
or_imp
theorem
: (a ∨ b → c) ↔ (a → c) ∧ (b → c)
Full source
theorem or_imp : (a ∨ b → c) ↔ (a → c) ∧ (b → c) :=
Iff.intro (fun h => ⟨h ∘ .inl, h ∘ .inr⟩) (fun ⟨ha, hb⟩ => Or.rec ha hb)Informal description
For any propositions $a$, $b$, and $c$, the implication $a \lor b \to c$ holds if and only if both $a \to c$ and $b \to c$ hold.
not_or
theorem
: ¬(p ∨ q) ↔ ¬p ∧ ¬q
Full source
@[simp] theorem not_or : ¬(p ∨ q)¬(p ∨ q) ↔ ¬p ∧ ¬q := or_impInformal description
For any propositions $p$ and $q$, the negation of their disjunction is equivalent to the conjunction of their negations, i.e., $\neg(p \lor q) \leftrightarrow \neg p \land \neg q$.
not_and_of_not_or_not
theorem
(h : ¬a ∨ ¬b) : ¬(a ∧ b)
Informal description
If either $\neg a$ or $\neg b$ holds, then $\neg (a \land b)$ holds.
ne_of_apply_ne
theorem
{α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y
Full source
theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
mt <| congrArg _Informal description
For any function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, if $f(x) \neq f(y)$, then $x \neq y$.
if_false_left
theorem
[h : Decidable p] : ite p False q ↔ ¬p ∧ q
Full source
@[simp]
theorem if_false_left [h : Decidable p] :
iteite p False q ↔ ¬p ∧ q := by cases h <;> (rename_i g; simp [g])Informal description
For any proposition $p$ with a decidability instance, the expression `if p then False else q` is equivalent to $\neg p \land q$.
if_false_right
theorem
[h : Decidable p] : ite p q False ↔ p ∧ q
Full source
@[simp]
theorem if_false_right [h : Decidable p] :
iteite p q False ↔ p ∧ q := by cases h <;> (rename_i g; simp [g])Informal description
For any proposition $p$ with a decidable instance and any proposition $q$, the expression `if p then q else False` is equivalent to $p \land q$.
if_true_left
theorem
[h : Decidable p] : ite p True q ↔ ¬p → q
Full source
@[simp low]
theorem if_true_left [h : Decidable p] :
iteite p True q ↔ ¬p → q := by cases h <;> (rename_i g; simp [g])Informal description
For any proposition `p` with a decidable instance, the expression `if p then True else q` is equivalent to `¬p → q`.
if_true_right
theorem
[h : Decidable p] : ite p q True ↔ p → q
Full source
@[simp low]
theorem if_true_right [h : Decidable p] :
iteite p q True ↔ p → q := by cases h <;> (rename_i g; simp [g])Informal description
For any proposition $p$ with a decidable instance and any proposition $q$, the expression `if p then q else True` is equivalent to the implication $p \to q$.
dite_not
theorem
[hn : Decidable (¬p)] [h : Decidable p] (x : ¬p → α) (y : ¬¬p → α) :
dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x
Informal description
For any proposition `p` with decidable negation and decidable truth value, and for any functions `x : ¬p → α` and `y : ¬¬p → α`, the dependent if-then-else expression `dite (¬p) x y` is equal to `dite p (fun h ↦ y (not_not_intro h)) x`.
ite_not
theorem
(p : Prop) [Decidable p] (x y : α) : ite (¬p) x y = ite p y x
Informal description
For any decidable proposition $p$ and any elements $x, y$ of type $\alpha$, the if-then-else expression $\text{ite}(\neg p, x, y)$ is equal to $\text{ite}(p, y, x)$.
ite_then_self
theorem
{p q : Prop} [h : Decidable p] : (if p then p else q) ↔ (¬p → q)
Full source
@[simp] theorem ite_then_self {p q : Prop} [h : Decidable p] : (if p then p else q) ↔ (¬p → q) := by
cases h <;> (rename_i g; simp [g])Informal description
For any decidable proposition $p$ and any proposition $q$, the statement "if $p$ holds then $p$ holds, otherwise $q$ holds" is equivalent to "$\neg p$ implies $q$". In symbols:
$$ (\text{if } p \text{ then } p \text{ else } q) \leftrightarrow (\neg p \to q) $$
ite_else_self
theorem
{p q : Prop} [h : Decidable p] : (if p then q else p) ↔ (p ∧ q)
Full source
@[simp] theorem ite_else_self {p q : Prop} [h : Decidable p] : (if p then q else p) ↔ (p ∧ q) := by
cases h <;> (rename_i g; simp [g])Informal description
For any decidable proposition $p$ and any proposition $q$, the statement "if $p$ holds then $q$ holds, otherwise $p$ holds" is equivalent to "$p$ and $q$ both hold". In symbols:
$$ (\text{if } p \text{ then } q \text{ else } p) \leftrightarrow (p \land q) $$
ite_then_not_self
theorem
{p : Prop} [Decidable p] {q : Prop} : (if p then ¬p else q) ↔ ¬p ∧ q
Full source
@[simp] theorem ite_then_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then ¬p else q) ↔ ¬p ∧ q := by
split <;> simp_allInformal description
For any decidable proposition $p$ and any proposition $q$, the statement "if $p$ holds then $\neg p$ holds, otherwise $q$ holds" is equivalent to "$\neg p$ and $q$ both hold". In symbols:
$$ (\text{if } p \text{ then } \neg p \text{ else } q) \leftrightarrow (\neg p \land q) $$
ite_else_not_self
theorem
{p : Prop} [Decidable p] {q : Prop} : (if p then q else ¬p) ↔ p → q
Full source
@[simp] theorem ite_else_not_self {p : Prop} [Decidable p] {q : Prop} : (if p then q else ¬p) ↔ p → q := by
split <;> simp_allInformal description
For any propositions $p$ and $q$, where $p$ is decidable, the statement "if $p$ then $q$ else not $p$" is equivalent to the implication "$p$ implies $q$". In symbols:
$$ \text{if } p \text{ then } q \text{ else } \neg p \quad \leftrightarrow \quad p \to q $$
ite_eq_ite
theorem
(p : Prop) {h h' : Decidable p} (x y : α) : (@ite _ p h x y = @ite _ p h' x y) ↔ True
Full source
/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal. -/
-- This is useful for ensuring confluence, but rarely otherwise.
@[simp] theorem ite_eq_ite (p : Prop) {h h' : Decidable p} (x y : α) :
(@ite _ p h x y = @ite _ p h' x y) ↔ True := by
simp
congrInformal description
For any proposition $p$ and any elements $x, y$ of a type $\alpha$, the two if-then-else expressions `if p then x else y` constructed using different `Decidable` instances for $p$ are equal, and this equivalence holds trivially (i.e., it is equivalent to `True`).
ite_iff_ite
theorem
(p : Prop) {h h' : Decidable p} (x y : Prop) : (@ite _ p h x y ↔ @ite _ p h' x y) ↔ True
Full source
/-- If two if-then-else statements only differ by the `Decidable` instances, they are equal. -/
-- This is useful for ensuring confluence, but rarely otherwise.
@[simp] theorem ite_iff_ite (p : Prop) {h h' : Decidable p} (x y : Prop) :
(@ite _ p h x y ↔ @ite _ p h' x y) ↔ True := by
rw [iff_true]
suffices @ite _ p h x y = @ite _ p h' x y by simp [this]
congrInformal description
For any proposition $p$ with two different decidability instances $h$ and $h'$, and for any propositions $x$ and $y$, the two if-then-else expressions `if p then x else y` constructed with $h$ and $h'$ are logically equivalent if and only if the true proposition holds.
forall_imp
theorem
(h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a
Full source
theorem forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a := fun h' a => h a (h' a)Informal description
For any predicate $p$ and $q$ on a type, if for every element $a$, $p(a)$ implies $q(a)$, then the universal quantification of $p$ implies the universal quantification of $q$. In other words:
$$(\forall a, p(a) \to q(a)) \to (\forall a, p(a)) \to \forall a, q(a)$$
forall_exists_index
theorem
{q : (∃ x, p x) → Prop} : (∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩
Full source
/--
As `simp` does not index foralls, this `@[simp]` lemma is tried on every `forall` expression.
This is not ideal, and likely a performance issue, but it is difficult to remove this attribute at this time.
-/
@[simp] theorem forall_exists_index {q : (∃ x, p x) → Prop} :
(∀ h, q h) ↔ ∀ x (h : p x), q ⟨x, h⟩ :=
⟨fun h x hpx => h ⟨x, hpx⟩, fun h ⟨x, hpx⟩ => h x hpx⟩Informal description
For any predicate $q$ depending on an existential statement $\exists x, p(x)$, the universal quantification $\forall h, q(h)$ is equivalent to $\forall x (h : p(x)), q(\langle x, h \rangle)$.
In other words, a statement that holds for all proofs of $\exists x, p(x)$ is equivalent to a statement that holds for all $x$ and all proofs $h$ that $p(x)$ holds, where the existential witness is explicitly constructed as $\langle x, h \rangle$.
Exists.imp
theorem
(h : ∀ a, p a → q a) : (∃ a, p a) → ∃ a, q a
Full source
theorem Exists.imp (h : ∀ a, p a → q a) : (∃ a, p a) → ∃ a, q a
| ⟨a, hp⟩ => ⟨a, h a hp⟩Informal description
For any predicates $p$ and $q$ on a type, if for every element $a$, $p(a)$ implies $q(a)$, then the existence of an $a$ satisfying $p(a)$ implies the existence of an $a$ satisfying $q(a)$. In other words:
$$(\forall a, p(a) \to q(a)) \to (\exists a, p(a)) \to \exists a, q(a)$$
Exists.imp'
theorem
{β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a)) : (∃ a, p a) → ∃ b, q b
Full source
theorem Exists.imp' {β} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a)) :
(∃ a, p a) → ∃ b, q b
| ⟨_, hp⟩ => ⟨_, hpq _ hp⟩Informal description
Let $f : \alpha \to \beta$ be a function and $q : \beta \to \text{Prop}$ a predicate. If for every $a \in \alpha$, $p(a)$ implies $q(f(a))$, then the existence of an $a \in \alpha$ satisfying $p(a)$ implies the existence of a $b \in \beta$ satisfying $q(b)$.
exists_imp
theorem
: ((∃ x, p x) → b) ↔ ∀ x, p x → b
Full source
theorem exists_imp : ((∃ x, p x) → b) ↔ ∀ x, p x → b := forall_exists_indexInformal description
For any predicate $p$ on a type and any proposition $b$, the implication $(\exists x, p(x)) \to b$ is equivalent to $\forall x, p(x) \to b$.
exists₂_imp
theorem
{P : (x : α) → p x → Prop} : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b
Full source
theorem exists₂_imp {P : (x : α) → p x → Prop} : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b := by simpInformal description
For any predicate $P$ depending on $x : \alpha$ and a proof $h$ of $p(x)$, the statement that the existence of $x$ and $h$ such that $P(x,h)$ implies $b$ is equivalent to the statement that for all $x$ and $h$, $P(x,h)$ implies $b$. In symbols:
$$(\exists x\ \exists h, P(x,h)) \to b \quad \leftrightarrow \quad \forall x\ \forall h, P(x,h) \to b$$
exists_const
theorem
(α) [i : Nonempty α] : (∃ _ : α, b) ↔ b
Full source
@[simp] theorem exists_const (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩Informal description
For any nonempty type $\alpha$ and any proposition $b$, the statement "there exists an element in $\alpha$ such that $b$ holds" is equivalent to $b$ itself. In other words, $(\exists x : \alpha, b) \leftrightarrow b$.
exists_prop_congr
theorem
{p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') : Exists q ↔ ∃ h : p', q' (hp.2 h)
Full source
@[congr]
theorem exists_prop_congr {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
ExistsExists q ↔ ∃ h : p', q' (hp.2 h) :=
⟨fun ⟨_, _⟩ ↦ ⟨hp.1 ‹_›, (hq _).1 ‹_›⟩, fun ⟨_, _⟩ ↦ ⟨_, (hq _).2 ‹_›⟩⟩Informal description
For any propositions $p$ and $p'$, and any families of propositions $q : p \to \text{Prop}$ and $q' : p' \to \text{Prop}$, if for all $h$, $q(h)$ is equivalent to $q'(h)$, and $p$ is equivalent to $p'$, then the existence of an $h$ in $p$ such that $q(h)$ holds is equivalent to the existence of an $h$ in $p'$ such that $q'(h)$ holds.
In symbols:
If $\forall h, q(h) \leftrightarrow q'(h)$ and $p \leftrightarrow p'$, then $(\exists h \in p, q(h)) \leftrightarrow (\exists h \in p', q'(h))$.
exists_prop_of_true
theorem
{p : Prop} {q : p → Prop} (h : p) : (Exists fun h' : p => q h') ↔ q h
Full source
theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (Exists fun h' : p => q h') ↔ q h :=
@exists_const (q h) p ⟨h⟩Informal description
For any proposition $p$ and any predicate $q$ depending on $p$, if $p$ holds (i.e., $h : p$ is given), then the statement "there exists $h' : p$ such that $q(h')$ holds" is equivalent to $q(h)$.
exists_true_left
theorem
{p : True → Prop} : Exists p ↔ p True.intro
Full source
@[simp] theorem exists_true_left {p : True → Prop} : ExistsExists p ↔ p True.intro :=
exists_prop_of_true _Informal description
For any predicate $p$ depending on the trivial proposition `True`, the statement "there exists a proof $h$ of `True` such that $p(h)$ holds" is equivalent to $p(\text{True.intro})$, where $\text{True.intro}$ is the canonical proof of `True$.
forall_congr'
theorem
(h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a
Full source
theorem forall_congr' (h : ∀ a, p a ↔ q a) : (∀ a, p a) ↔ ∀ a, q a :=
⟨fun H a => (h a).1 (H a), fun H a => (h a).2 (H a)⟩Informal description
For any predicate `p` and `q` depending on a parameter `a`, if for every `a` the statements `p a` and `q a` are equivalent, then the universal quantification `∀ a, p a` is equivalent to `∀ a, q a`.
exists_congr
theorem
(h : ∀ a, p a ↔ q a) : (∃ a, p a) ↔ ∃ a, q a
Full source
theorem exists_congr (h : ∀ a, p a ↔ q a) : (∃ a, p a) ↔ ∃ a, q a :=
⟨Exists.imp fun x => (h x).1, Exists.imp fun x => (h x).2⟩Informal description
For any predicates $p$ and $q$ on a type, if for every element $a$, $p(a)$ is equivalent to $q(a)$, then the existence of an $a$ satisfying $p(a)$ is equivalent to the existence of an $a$ satisfying $q(a)$. In other words:
$$(\forall a, p(a) \leftrightarrow q(a)) \to (\exists a, p(a)) \leftrightarrow (\exists a, q(a))$$
forall₂_congr
theorem
{p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) : (∀ a b, p a b) ↔ ∀ a b, q a b
Full source
theorem forall₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
(∀ a b, p a b) ↔ ∀ a b, q a b :=
forall_congr' fun a => forall_congr' <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$ and $b$, if for every $a$ and $b$ the statements $p(a, b)$ and $q(a, b)$ are equivalent, then the universal quantification $\forall a b, p(a, b)$ is equivalent to $\forall a b, q(a, b)$.
exists₂_congr
theorem
{p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) : (∃ a b, p a b) ↔ ∃ a b, q a b
Full source
theorem exists₂_congr {p q : ∀ a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
(∃ a b, p a b) ↔ ∃ a b, q a b :=
exists_congr fun a => exists_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$ and $b$, if for every $a$ and $b$ the statements $p(a, b)$ and $q(a, b)$ are equivalent, then the existential quantification $\exists a b, p(a, b)$ is equivalent to $\exists a b, q(a, b)$. In other words:
$$(\forall a b, p(a, b) \leftrightarrow q(a, b)) \to (\exists a b, p(a, b)) \leftrightarrow (\exists a b, q(a, b))$$
forall₃_congr
theorem
{p q : ∀ a b, γ a b → 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
Full source
theorem forall₃_congr {p q : ∀ a b, γ a b → 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 :=
forall_congr' fun a => forall₂_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, and $c$, if for every $a$, $b$, and $c$ the statements $p(a, b, c)$ and $q(a, b, c)$ are equivalent, then the universal quantification $\forall a b c, p(a, b, c)$ is equivalent to $\forall a b c, q(a, b, c)$.
exists₃_congr
theorem
{p q : ∀ a b, γ a b → 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
Full source
theorem exists₃_congr {p q : ∀ a b, γ a b → 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 :=
exists_congr fun a => exists₂_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, and $c$, if for every $a$, $b$, and $c$ the statements $p(a, b, c)$ and $q(a, b, c)$ are equivalent, then the existential quantification $\exists a b c, p(a, b, c)$ is equivalent to $\exists a b c, q(a, b, c)$. In other words:
$$(\forall a b c, p(a, b, c) \leftrightarrow q(a, b, c)) \to (\exists a b c, p(a, b, c)) \leftrightarrow (\exists a b c, q(a, b, c))$$
forall₄_congr
theorem
{p q : ∀ a b c, δ a b c → 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
Full source
theorem forall₄_congr {p q : ∀ a b c, δ a b c → 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 :=
forall_congr' fun a => forall₃_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, $c$, and $d$, if for every $a$, $b$, $c$, and $d$ the statements $p(a, b, c, d)$ and $q(a, b, c, d)$ are equivalent, then the universal quantification $\forall a b c d, p(a, b, c, d)$ is equivalent to $\forall a b c d, q(a, b, c, d)$.
exists₄_congr
theorem
{p q : ∀ a b c, δ a b c → 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
Full source
theorem exists₄_congr {p q : ∀ a b c, δ a b c → 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 :=
exists_congr fun a => exists₃_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, $c$, and $d$, if for every $a$, $b$, $c$, and $d$ the statements $p(a, b, c, d)$ and $q(a, b, c, d)$ are equivalent, then the existential quantification $\exists a b c d, p(a, b, c, d)$ is equivalent to $\exists a b c d, q(a, b, c, d)$. In other words:
$$(\forall a b c d, p(a, b, c, d) \leftrightarrow q(a, b, c, d)) \to (\exists a b c d, p(a, b, c, d)) \leftrightarrow (\exists a b c d, q(a, b, c, d))$$
forall₅_congr
theorem
{p q : ∀ a b c d, ε a b c d → Prop} (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
(∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e
Full source
theorem forall₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
(h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
(∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e :=
forall_congr' fun a => forall₄_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, $c$, $d$, and $e$, if for every $a$, $b$, $c$, $d$, and $e$ the statements $p(a, b, c, d, e)$ and $q(a, b, c, d, e)$ are equivalent, then the universal quantification $\forall a b c d e, p(a, b, c, d, e)$ is equivalent to $\forall a b c d e, q(a, b, c, d, e)$.
exists₅_congr
theorem
{p q : ∀ a b c d, ε a b c d → Prop} (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
(∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e
Full source
theorem exists₅_congr {p q : ∀ a b c d, ε a b c d → Prop}
(h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
(∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e :=
exists_congr fun a => exists₄_congr <| h aInformal description
For any two families of predicates $p$ and $q$ depending on parameters $a$, $b$, $c$, $d$, and $e$, if for every $a$, $b$, $c$, $d$, and $e$ the statements $p(a, b, c, d, e)$ and $q(a, b, c, d, e)$ are equivalent, then the existential quantification $\exists a b c d e, p(a, b, c, d, e)$ is equivalent to $\exists a b c d e, q(a, b, c, d, e)$. In symbols:
$$(\forall a b c d e, p(a, b, c, d, e) \leftrightarrow q(a, b, c, d, e)) \to (\exists a b c d e, p(a, b, c, d, e)) \leftrightarrow (\exists a b c d e, q(a, b, c, d, e))$$
not_exists
theorem
: (¬∃ x, p x) ↔ ∀ x, ¬p x
Full source
@[simp] theorem not_exists : (¬∃ x, p x) ↔ ∀ x, ¬p x := exists_impInformal description
For any predicate $p$ on a type, the statement "there does not exist an $x$ such that $p(x)$ holds" is equivalent to "for all $x$, $p(x)$ does not hold". In symbols:
$$\neg (\exists x, p(x)) \leftrightarrow \forall x, \neg p(x)$$
forall_not_of_not_exists
theorem
(h : ¬∃ x, p x) : ∀ x, ¬p x
Full source
theorem forall_not_of_not_exists (h : ¬∃ x, p x) : ∀ x, ¬p x := not_exists.mp hInformal description
If there does not exist an $x$ such that $p(x)$ holds, then for all $x$, $p(x)$ does not hold. In symbols:
$$(\neg \exists x, p(x)) \rightarrow (\forall x, \neg p(x))$$
not_exists_of_forall_not
theorem
(h : ∀ x, ¬p x) : ¬∃ x, p x
Full source
theorem not_exists_of_forall_not (h : ∀ x, ¬p x) : ¬∃ x, p x := not_exists.mpr hInformal description
For any predicate $p$ on a type, if for all $x$, $p(x)$ does not hold, then there does not exist an $x$ such that $p(x)$ holds. In symbols:
$$(\forall x, \neg p(x)) \rightarrow \neg (\exists x, p(x))$$
forall_and
theorem
: (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x)
Informal description
For any predicate $p$ and $q$ on a type $\alpha$, the statement $(\forall x, p(x) \land q(x))$ holds if and only if both $(\forall x, p(x))$ and $(\forall x, q(x))$ hold.
exists_or
theorem
: (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
Informal description
There exists an element $x$ such that $p(x)$ or $q(x)$ holds if and only if there exists an element $x$ such that $p(x)$ holds or there exists an element $x$ such that $q(x)$ holds.
exists_false
theorem
: ¬(∃ _a : α, False)
Full source
@[simp] theorem exists_false : ¬(∃ _a : α, False) := fun ⟨_, h⟩ => hInformal description
There does not exist an element $a$ of type $\alpha$ such that the false proposition holds, i.e., $\neg (\exists a : \alpha, \text{False})$.
forall_const
theorem
(α : Sort _) [i : Nonempty α] : (α → b) ↔ b
Full source
@[simp] theorem forall_const (α : Sort _) [i : Nonempty α] : (α → b) ↔ b :=
⟨i.elim, fun hb _ => hb⟩Informal description
For any nonempty type $\alpha$ and any proposition $b$, the universal quantification $(\forall x : \alpha, b)$ is equivalent to $b$. In other words, a constant predicate over a nonempty domain is equivalent to the constant itself.
Exists.nonempty
theorem
: (∃ x, p x) → Nonempty α
Full source
theorem Exists.nonempty : (∃ x, p x) → Nonempty α | ⟨x, _⟩ => ⟨x⟩Informal description
If there exists an element $x$ in a type $\alpha$ such that the property $p(x)$ holds, then the type $\alpha$ is nonempty.
not_forall_of_exists_not
theorem
{p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x
Full source
theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x, p x
| ⟨x, hn⟩, h => hn (h x)Informal description
For any predicate $p$ on a type $\alpha$, if there exists an element $x$ such that $\neg p(x)$ holds, then it is not the case that $p(x)$ holds for all $x$.
forall_eq
theorem
{p : α → Prop} {a' : α} : (∀ a, a = a' → p a) ↔ p a'
Full source
@[simp] theorem forall_eq {p : α → Prop} {a' : α} : (∀ a, a = a' → p a) ↔ p a' :=
⟨fun h => h a' rfl, fun h _ e => e.symm ▸ h⟩Informal description
For any predicate $p$ on a type $\alpha$ and any element $a' \in \alpha$, the universal quantification $(\forall a, a = a' \to p(a))$ is equivalent to $p(a')$. In other words, the statement "for all $a$ equal to $a'$, $p(a)$ holds" is equivalent to "$p(a')$ holds".
forall_eq'
theorem
{a' : α} : (∀ a, a' = a → p a) ↔ p a'
Full source
@[simp] theorem forall_eq' {a' : α} : (∀ a, a' = a → p a) ↔ p a' := by simp [@eq_comm _ a']Informal description
For any element $a'$ of type $\alpha$, the universal statement "for all $a$, if $a' = a$ then $p(a)$ holds" is equivalent to the statement $p(a')$ holding.
exists_eq
theorem
: ∃ a, a = a'
Full source
@[simp] theorem exists_eq : ∃ a, a = a' := ⟨_, rfl⟩Informal description
There exists an element $a$ such that $a = a'$.
exists_eq'
theorem
: ∃ a, a' = a
Full source
@[simp] theorem exists_eq' : ∃ a, a' = a := ⟨_, rfl⟩Informal description
There exists an element $a$ such that $a' = a$.
exists_eq_left
theorem
: (∃ a, a = a' ∧ p a) ↔ p a'
Full source
@[simp] theorem exists_eq_left : (∃ a, a = a' ∧ p a) ↔ p a' :=
⟨fun ⟨_, e, h⟩ => e ▸ h, fun h => ⟨_, rfl, h⟩⟩Informal description
For any predicate $p$ and element $a'$, the statement that there exists an element $a$ such that $a = a'$ and $p(a)$ holds is equivalent to $p(a')$ holding.
exists_eq_right
theorem
: (∃ a, p a ∧ a = a') ↔ p a'
Full source
@[simp] theorem exists_eq_right : (∃ a, p a ∧ a = a') ↔ p a' :=
(exists_congr <| by exact fun a => And.comm).trans exists_eq_leftInformal description
For any predicate $p$ and element $a'$, the statement that there exists an element $a$ such that $p(a)$ holds and $a = a'$ is equivalent to $p(a')$ holding. In other words:
$$(\exists a, p(a) \land a = a') \leftrightarrow p(a')$$
exists_and_left
theorem
: (∃ x, b ∧ p x) ↔ b ∧ (∃ x, p x)
Full source
@[simp] theorem exists_and_left : (∃ x, b ∧ p x) ↔ b ∧ (∃ x, p x) :=
⟨fun ⟨x, h, hp⟩ => ⟨h, x, hp⟩, fun ⟨h, x, hp⟩ => ⟨x, h, hp⟩⟩Informal description
There exists an element $x$ such that both $b$ and $p(x)$ hold if and only if $b$ holds and there exists an element $x$ such that $p(x)$ holds.
exists_and_right
theorem
: (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b
Full source
@[simp] theorem exists_and_right : (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b := by simp [And.comm]Informal description
For any predicate $p$ and proposition $b$, there exists an element $x$ such that $p(x)$ and $b$ hold if and only if there exists an element $x$ such that $p(x)$ holds and $b$ holds. In other words:
$$
(\exists x, p(x) \land b) \leftrightarrow (\exists x, p(x)) \land b
$$
exists_eq_left'
theorem
: (∃ a, a' = a ∧ p a) ↔ p a'
Full source
@[simp] theorem exists_eq_left' : (∃ a, a' = a ∧ p a) ↔ p a' := by simp [@eq_comm _ a']Informal description
There exists an element $a$ such that $a' = a$ and $p(a)$ holds if and only if $p(a')$ holds.
exists_eq_right'
theorem
: (∃ a, p a ∧ a' = a) ↔ p a'
Full source
@[simp] theorem exists_eq_right' : (∃ a, p a ∧ a' = a) ↔ p a' := by simp [@eq_comm _ a']Informal description
There exists an element $a$ such that $p(a)$ holds and $a' = a$ if and only if $p(a')$ holds.
forall_eq_or_imp
theorem
: (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a
Full source
@[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by
simp only [or_imp, forall_and, forall_eq]Informal description
For any predicate $p$ and $q$ on a type $\alpha$ and any element $a' \in \alpha$, the following equivalence holds:
\[
(\forall a, (a = a' \lor q(a)) \to p(a)) \leftrightarrow (p(a') \land (\forall a, q(a) \to p(a)))
\]
exists_eq_or_imp
theorem
: (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a
Full source
@[simp] theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by
simp only [or_and_right, exists_or, exists_eq_left]Informal description
For any predicate $p$ and $q$ on a type $\alpha$, and for any element $a'$ of $\alpha$, the following equivalence holds:
\[
(\exists a, (a = a' \lor q a) \land p a) \leftrightarrow (p a' \lor \exists a, q a \land p a)
\]
exists_eq_right_right
theorem
: (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'
Full source
@[simp] theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a' := by
simp [← and_assoc]Informal description
For any type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the following equivalence holds:
$$(\exists a \in \alpha,\; p(a) \land q(a) \land a = a') \;\leftrightarrow\; p(a') \land q(a').$$
exists_eq_right_right'
theorem
: (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'
Full source
@[simp] theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a' := by
simp [@eq_comm _ a']Informal description
For any predicate functions $p$ and $q$ on a type $\alpha$ and any element $a' \in \alpha$, the following are equivalent:
1. There exists an element $a \in \alpha$ such that $p(a)$, $q(a)$, and $a' = a$.
2. Both $p(a')$ and $q(a')$ hold.
exists_or_eq_left
theorem
(y : α) (p : α → Prop) : ∃ x : α, x = y ∨ p x
Full source
@[simp] theorem exists_or_eq_left (y : α) (p : α → Prop) : ∃ x : α, x = y ∨ p x := ⟨y, .inl rfl⟩Informal description
For any element $y$ of type $\alpha$ and any predicate $p$ on $\alpha$, there exists an element $x$ in $\alpha$ such that either $x = y$ or $p(x)$ holds.
exists_or_eq_right
theorem
(y : α) (p : α → Prop) : ∃ x : α, p x ∨ x = y
Full source
@[simp] theorem exists_or_eq_right (y : α) (p : α → Prop) : ∃ x : α, p x ∨ x = y := ⟨y, .inr rfl⟩Informal description
For any element $y$ of type $\alpha$ and any predicate $p$ on $\alpha$, there exists an element $x$ in $\alpha$ such that either $p(x)$ holds or $x$ is equal to $y$.
exists_or_eq_left'
theorem
(y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x
Full source
@[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩Informal description
For any element $y$ of type $\alpha$ and any predicate $p$ on $\alpha$, there exists an element $x$ in $\alpha$ such that either $y = x$ or $p(x)$ holds.
exists_or_eq_right'
theorem
(y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x
Full source
@[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩Informal description
For any element $y$ of type $\alpha$ and any predicate $p$ on $\alpha$, there exists an element $x$ in $\alpha$ such that either $p(x)$ holds or $y = x$.
exists_prop'
theorem
{p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p
Full source
theorem exists_prop' {p : Prop} : (∃ _ : α, p) ↔ Nonempty α ∧ p :=
⟨fun ⟨a, h⟩ => ⟨⟨a⟩, h⟩, fun ⟨⟨a⟩, h⟩ => ⟨a, h⟩⟩Informal description
For any proposition $p$, the statement "there exists an element of type $\alpha$ such that $p$ holds" is equivalent to "the type $\alpha$ is nonempty and $p$ holds", i.e.,
$$ (\exists x : \alpha, p) \leftrightarrow (\text{Nonempty } \alpha \land p). $$
exists_prop
theorem
: (∃ _h : a, b) ↔ a ∧ b
Full source
@[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩Informal description
For any propositions $a$ and $b$, the statement "there exists a proof of $a$ such that $b$ holds" is equivalent to "$a$ and $b$ both hold", i.e.,
$$ (\exists \_h : a, b) \leftrightarrow a \land b. $$
exists_idem
theorem
{P : Prop} (f : P → P → Sort _) : (∃ (p₁ : P), ∃ (p₂ : P), f p₁ p₂) ↔ ∃ (p : P), f p p
Full source
@[simp] theorem exists_idem {P : Prop} (f : P → P → Sort _) :
(∃ (p₁ : P), ∃ (p₂ : P), f p₁ p₂) ↔ ∃ (p : P), f p p :=
⟨fun ⟨p, _, h⟩ => ⟨p, h⟩, fun ⟨p, h⟩ => ⟨p, p, h⟩⟩Informal description
For any proposition $P$ and any function $f : P \to P \to \text{Sort}_*$, the following equivalence holds:
$$(\exists p_1 : P, \exists p_2 : P, f(p_1, p_2)) \leftrightarrow (\exists p : P, f(p, p)).$$
exists_apply_eq_apply
theorem
(f : α → β) (a' : α) : ∃ a, f a = f a'
Full source
@[simp] theorem exists_apply_eq_apply (f : α → β) (a' : α) : ∃ a, f a = f a' := ⟨a', rfl⟩Informal description
For any function $f \colon \alpha \to \beta$ and any element $a' \in \alpha$, there exists an element $a \in \alpha$ such that $f(a) = f(a')$.
forall_prop_of_true
theorem
{p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h
Full source
theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∀ h' : p, q h') ↔ q h :=
@forall_const (q h) p ⟨h⟩Informal description
For any proposition $p$ and any predicate $q$ on $p$, given a proof $h$ of $p$, the universal quantification $(\forall h' : p, q(h'))$ is equivalent to $q(h)$.
forall_comm
theorem
{p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b)
Full source
theorem forall_comm {p : α → β → Prop} : (∀ a b, p a b) ↔ (∀ b a, p a b) :=
⟨fun h b a => h a b, fun h a b => h b a⟩Informal description
For any binary predicate $p$ on types $\alpha$ and $\beta$, the universal quantification $(\forall a \in \alpha, \forall b \in \beta, p(a, b))$ holds if and only if $(\forall b \in \beta, \forall a \in \alpha, p(a, b))$ holds.
exists_comm
theorem
{p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b)
Full source
theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p a b) :=
⟨fun ⟨a, b, h⟩ => ⟨b, a, h⟩, fun ⟨b, a, h⟩ => ⟨a, b, h⟩⟩Informal description
For any binary relation $p$ on types $\alpha$ and $\beta$, the existential quantifiers can be swapped: there exists $a \in \alpha$ and $b \in \beta$ such that $p(a,b)$ holds if and only if there exists $b \in \beta$ and $a \in \alpha$ such that $p(a,b)$ holds.
forall_apply_eq_imp_iff
theorem
{f : α → β} {p : β → Prop} : (∀ b a, f a = b → p b) ↔ ∀ a, p (f a)
Full source
@[simp] theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
(∀ b a, f a = b → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]Informal description
For any function $f \colon \alpha \to \beta$ and predicate $p \colon \beta \to \mathrm{Prop}$, the following are equivalent:
1. For every $b \in \beta$ and $a \in \alpha$, if $f(a) = b$ then $p(b)$ holds.
2. For every $a \in \alpha$, $p(f(a))$ holds.
In other words, $(\forall b \, a, f(a) = b \to p(b)) \leftrightarrow (\forall a, p(f(a)))$.
forall_eq_apply_imp_iff
theorem
{f : α → β} {p : β → Prop} : (∀ b a, b = f a → p b) ↔ ∀ a, p (f a)
Full source
@[simp] theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} :
(∀ b a, b = f a → p b) ↔ ∀ a, p (f a) := by simp [forall_comm]Informal description
For any function $f : \alpha \to \beta$ and predicate $p : \beta \to \mathrm{Prop}$, the following are equivalent:
1. For all $b \in \beta$ and $a \in \alpha$, if $b = f(a)$ then $p(b)$ holds.
2. For all $a \in \alpha$, $p(f(a))$ holds.
In other words: $(\forall b\, a, b = f(a) \to p(b)) \leftrightarrow (\forall a, p(f(a)))$.
forall_apply_eq_imp_iff₂
theorem
{f : α → β} {p : α → Prop} {q : β → Prop} : (∀ b a, p a → f a = b → q b) ↔ ∀ a, p a → q (f a)
Full source
@[simp] theorem forall_apply_eq_imp_iff₂ {f : α → β} {p : α → Prop} {q : β → Prop} :
(∀ b a, p a → f a = b → q b) ↔ ∀ a, p a → q (f a) :=
⟨fun h a ha => h (f a) a ha rfl, fun h _ a ha hb => hb ▸ h a ha⟩Informal description
For any function $f \colon \alpha \to \beta$ and predicates $p \colon \alpha \to \mathrm{Prop}$, $q \colon \beta \to \mathrm{Prop}$, the following are equivalent:
1. For every $b \in \beta$ and $a \in \alpha$, if $p(a)$ holds and $f(a) = b$, then $q(b)$ holds.
2. For every $a \in \alpha$, if $p(a)$ holds, then $q(f(a))$ holds.
In other words: $(\forall b\, a, p(a) \to f(a) = b \to q(b)) \leftrightarrow (\forall a, p(a) \to q(f(a)))$.
forall_prop_of_false
theorem
{p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True
Full source
theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
iff_true_intro fun h => hn.elim hInformal description
For any proposition $p$ and any predicate $q$ depending on $p$, if $p$ is false (i.e., $\neg p$ holds), then the universal quantification $\forall (h' : p), q(h')$ is equivalent to $\text{True}$.
and_exists_self
theorem
(P : Prop) (Q : P → Prop) : (P ∧ ∃ p, Q p) ↔ ∃ p, Q p
Full source
@[simp] theorem and_exists_self (P : Prop) (Q : P → Prop) : (P ∧ ∃ p, Q p) ↔ ∃ p, Q p :=
⟨fun ⟨_, h⟩ => h, fun ⟨p, q⟩ => ⟨p, ⟨p, q⟩⟩⟩Informal description
For any proposition $P$ and any predicate $Q$ depending on $P$, the conjunction of $P$ and the existence of some $p$ such that $Q(p)$ holds is equivalent to the existence of some $p$ such that $Q(p)$ holds. In other words, $P \land (\exists p, Q(p)) \leftrightarrow \exists p, Q(p)$.
exists_and_self
theorem
(P : Prop) (Q : P → Prop) : ((∃ p, Q p) ∧ P) ↔ ∃ p, Q p
Full source
@[simp] theorem exists_and_self (P : Prop) (Q : P → Prop) : ((∃ p, Q p) ∧ P) ↔ ∃ p, Q p :=
⟨fun ⟨h, _⟩ => h, fun ⟨p, q⟩ => ⟨⟨p, q⟩, p⟩⟩Informal description
For any proposition $P$ and any predicate $Q$ depending on $P$, the conjunction of the existence of $p$ such that $Q(p)$ holds and $P$ itself is equivalent to the existence of $p$ such that $Q(p)$ holds. In other words:
$$ \left( (\exists p, Q(p)) \land P \right) \leftrightarrow \exists p, Q(p). $$
forall_self_imp
theorem
(P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p
Full source
@[simp] theorem forall_self_imp (P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p :=
⟨fun h p => h p p, fun h _ p => h p⟩Informal description
For any proposition $P$ and any predicate $Q$ depending on $P$, the statement $(\forall p : P, P \to Q(p))$ is equivalent to $(\forall p, Q(p))$.
ne_of_mem_of_not_mem
theorem
(h : a ∈ s) : b ∉ s → a ≠ b
Full source
theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ hInformal description
For any elements $a$ and $b$ and any set $s$, if $a$ is an element of $s$ and $b$ is not an element of $s$, then $a$ is not equal to $b$.
ne_of_mem_of_not_mem'
theorem
(h : a ∈ s) : a ∉ t → s ≠ t
Full source
theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ hInformal description
For any element $a$ and sets $s$ and $t$, if $a$ is an element of $s$ but not an element of $t$, then $s$ is not equal to $t$.
nonempty_prop
theorem
{p : Prop} : Nonempty p ↔ p
Full source
@[simp] theorem nonempty_prop {p : Prop} : NonemptyNonempty p ↔ p :=
⟨fun ⟨h⟩ => h, fun h => ⟨h⟩⟩Informal description
For any proposition $p$, the type `Nonempty p` (asserting that $p$ is inhabited) is equivalent to $p$ itself, i.e., $\text{Nonempty } p \leftrightarrow p$.
Decidable.not_not
theorem
[Decidable p] : ¬¬p ↔ p
Full source
@[simp] theorem Decidable.not_not [Decidable p] : ¬¬p¬¬p ↔ p := ⟨of_not_not, not_not_intro⟩Informal description
For any decidable proposition $p$, the double negation of $p$ is equivalent to $p$, i.e., $\neg \neg p \leftrightarrow p$.
Decidable.or_not_self
abbrev
Full source
/-- Excluded middle. Added as alias for Decidable.em -/
abbrev Decidable.or_not_self := emInformal description
For any decidable proposition $p$, the disjunction $p \lor \neg p$ holds.
Decidable.not_or_self
theorem
(p : Prop) [h : Decidable p] : ¬p ∨ p
Full source
/-- Excluded middle commuted. Added as alias for Decidable.em -/
theorem Decidable.not_or_self (p : Prop) [h : Decidable p] : ¬p¬p ∨ p := by
cases h <;> simp [*]Informal description
For any decidable proposition $p$, either $p$ is false or $p$ is true, i.e., $\neg p \lor p$.
Decidable.by_contra
theorem
[Decidable p] : (¬p → False) → p
Full source
theorem Decidable.by_contra [Decidable p] : (¬p → False) → p := of_not_notInformal description
For any decidable proposition $p$, if assuming $\neg p$ leads to a contradiction, then $p$ holds.
Or.by_cases
definition
[Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α
Full source
/-- Construct a non-Prop by cases on an `Or`, when the left conjunct is decidable. -/
protected def Or.by_cases [Decidable p] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
if hp : p then h₁ hp else h₂ (h.resolve_left hp)Informal description
Given a decidable proposition \( p \), a type \( \alpha \), and a disjunction \( h : p \lor q \), the function `Or.by_cases` constructs an element of \( \alpha \) by cases: if \( p \) holds (as determined by the decidability instance), it applies \( h_1 : p \to \alpha \); otherwise, it applies \( h_2 : q \to \alpha \) to the proof that \( q \) must hold (since \( p \) does not).
Or.by_cases'
definition
[Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α
Full source
/-- Construct a non-Prop by cases on an `Or`, when the right conjunct is decidable. -/
protected def Or.by_cases' [Decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : q → α) : α :=
if hq : q then h₂ hq else h₁ (h.resolve_right hq)Informal description
Given a decidable proposition \( q \), a disjunction \( p \lor q \), and two functions \( h_1 : p \to \alpha \) and \( h_2 : q \to \alpha \), the function `Or.by_cases'` constructs an element of type \( \alpha \) by cases on the disjunction. If \( q \) holds, it applies \( h_2 \) to the proof of \( q \); otherwise, it applies \( h_1 \) to the proof of \( p \) obtained by resolving the disjunction \( p \lor q \) against the negation of \( q \).
exists_prop_decidable
instance
{p} (P : p → Prop) [Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h)
Full source
instance exists_prop_decidable {p} (P : p → Prop)
[Decidable p] [∀ h, Decidable (P h)] : Decidable (∃ h, P h) :=
if h : p then
decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
else isFalse fun ⟨h', _⟩ => h h'Informal description
For any proposition $p$ and predicate $P$ on $p$, if $p$ is decidable and for every proof $h$ of $p$, $P(h)$ is decidable, then the existential statement $\exists h, P(h)$ is decidable.
forall_prop_decidable
instance
{p} (P : p → Prop) [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h)
Full source
instance forall_prop_decidable {p} (P : p → Prop)
[Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
if h : p then
decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩
else isTrue fun h2 => absurd h2 hInformal description
For any proposition $p$ and predicate $P$ on $p$, if $p$ is decidable and for every proof $h$ of $p$, $P(h)$ is decidable, then the universal quantification $\forall h, P(h)$ is decidable.
decide_eq_true_iff
theorem
{p : Prop} [Decidable p] : (decide p = true) ↔ p
Full source
@[bool_to_prop] theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p := by simpInformal description
For any decidable proposition $p$, the decision procedure `decide p` returns `true` if and only if $p$ holds.
decide_eq_decide
theorem
{p q : Prop} {_ : Decidable p} {_ : Decidable q} : decide p = decide q ↔ (p ↔ q)
Full source
@[simp, bool_to_prop] theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
decidedecide p = decide q ↔ (p ↔ q) :=
⟨fun h => by rw [← decide_eq_true_iff (p := p), h, decide_eq_true_iff], fun h => by simp [h]⟩Informal description
For any decidable propositions $p$ and $q$, the equality $\text{decide}(p) = \text{decide}(q)$ holds if and only if $p$ and $q$ are logically equivalent, i.e., $p \leftrightarrow q$.
Decidable.of_not_imp
theorem
[Decidable a] (h : ¬(a → b)) : a
Full source
theorem Decidable.of_not_imp [Decidable a] (h : ¬(a → b)) : a :=
byContradiction (not_not_of_not_imp h)Informal description
For any decidable propositions $a$ and $b$, if $\neg(a \to b)$ holds, then $a$ holds.
Decidable.not_imp_symm
theorem
[Decidable a] (h : ¬a → b) (hb : ¬b) : a
Full source
theorem Decidable.not_imp_symm [Decidable a] (h : ¬a → b) (hb : ¬b) : a :=
byContradiction <| hb ∘ hInformal description
For any decidable proposition $a$ and any proposition $b$, if $\neg a$ implies $b$ and $\neg b$ holds, then $a$ must be true.
Decidable.not_imp_comm
theorem
[Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a)
Full source
theorem Decidable.not_imp_comm [Decidable a] [Decidable b] : (¬a → b) ↔ (¬b → a) :=
⟨not_imp_symm, not_imp_symm⟩Informal description
For any decidable propositions $a$ and $b$, the implication $\neg a \to b$ is equivalent to the implication $\neg b \to a$.
Decidable.not_imp_self
theorem
[Decidable a] : (¬a → a) ↔ a
Full source
theorem Decidable.not_imp_self [Decidable a] : (¬a → a) ↔ a := by
have := @imp_not_self (¬a); rwa [not_not] at thisInformal description
For any decidable proposition $a$, the implication $\neg a \to a$ is equivalent to $a$, i.e., $(\neg a \to a) \leftrightarrow a$.
Decidable.or_iff_not_imp_left
theorem
[Decidable a] : a ∨ b ↔ (¬a → b)
Full source
theorem Decidable.or_iff_not_imp_left [Decidable a] : a ∨ ba ∨ b ↔ (¬a → b) :=
⟨Or.resolve_left, fun h => dite _ .inl (.inr ∘ h)⟩Informal description
For decidable propositions $a$ and $b$, the disjunction $a \lor b$ holds if and only if the implication $\neg a \to b$ holds.
Decidable.or_iff_not_imp_right
theorem
[Decidable b] : a ∨ b ↔ (¬b → a)
Full source
theorem Decidable.or_iff_not_imp_right [Decidable b] : a ∨ ba ∨ b ↔ (¬b → a) :=
or_comm.trans or_iff_not_imp_leftInformal description
For decidable propositions $a$ and $b$, the disjunction $a \lor b$ holds if and only if the implication $\neg b \to a$ holds.
Decidable.not_imp_not
theorem
[Decidable a] : (¬a → ¬b) ↔ (b → a)
Full source
theorem Decidable.not_imp_not [Decidable a] : (¬a → ¬b) ↔ (b → a) :=
⟨fun h hb => byContradiction (h · hb), mt⟩Informal description
For a decidable proposition $a$, the implication $\neg a \to \neg b$ is equivalent to $b \to a$.
Decidable.not_or_of_imp
theorem
[Decidable a] (h : a → b) : ¬a ∨ b
Full source
theorem Decidable.not_or_of_imp [Decidable a] (h : a → b) : ¬a¬a ∨ b :=
if ha : a then .inr (h ha) else .inl haInformal description
For any decidable propositions $a$ and $b$, if $a$ implies $b$ ($a \to b$), then either $a$ is false ($\neg a$) or $b$ is true ($b$).
Decidable.imp_iff_not_or
theorem
[Decidable a] : (a → b) ↔ (¬a ∨ b)
Full source
theorem Decidable.imp_iff_not_or [Decidable a] : (a → b) ↔ (¬a ∨ b) :=
⟨not_or_of_imp, Or.neg_resolve_left⟩Informal description
For any decidable proposition $a$, the implication $a \to b$ is equivalent to $\neg a \lor b$.
Decidable.imp_iff_or_not
theorem
[Decidable b] : b → a ↔ a ∨ ¬b
Full source
theorem Decidable.imp_iff_or_not [Decidable b] : b → a ↔ a ∨ ¬b :=
Decidable.imp_iff_not_or.trans or_commInformal description
For any decidable proposition $b$, the implication $b \to a$ is equivalent to $a \lor \neg b$.
Decidable.imp_or
theorem
[Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c)
Informal description
For a decidable proposition $a$, the implication $a \to (b \lor c)$ is equivalent to $(a \to b) \lor (a \to c)$.
Decidable.imp_or'
theorem
[Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c)
Informal description
For any propositions $a$, $b$, and $c$, with $b$ being decidable, the implication $a \to (b \lor c)$ is equivalent to $(a \to b) \lor (a \to c)$.
Decidable.not_imp_iff_and_not
theorem
[Decidable a] : ¬(a → b) ↔ a ∧ ¬b
Full source
theorem Decidable.not_imp_iff_and_not [Decidable a] : ¬(a → b)¬(a → b) ↔ a ∧ ¬b :=
⟨fun h => ⟨of_not_imp h, not_of_not_imp h⟩, not_imp_of_and_not⟩Informal description
For any decidable proposition $a$ and any proposition $b$, the negation of the implication $a \to b$ is equivalent to the conjunction of $a$ and the negation of $b$, i.e., $\neg(a \to b) \leftrightarrow (a \land \neg b)$.
Decidable.peirce
theorem
(a b : Prop) [Decidable a] : ((a → b) → a) → a
Full source
theorem Decidable.peirce (a b : Prop) [Decidable a] : ((a → b) → a) → a :=
if ha : a then fun _ => ha else fun h => h ha.elimInformal description
For any propositions $a$ and $b$, where $a$ is decidable, the implication $((a \to b) \to a) \to a$ holds.
peirce'
theorem
{a : Prop} (H : ∀ b : Prop, (a → b) → a) : a
Informal description
For any proposition $a$, if for every proposition $b$ the implication $(a \to b) \to a$ holds, then $a$ holds.
Decidable.not_iff_not
theorem
[Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b)
Full source
theorem Decidable.not_iff_not [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b) := by
rw [@iff_def (¬a), @iff_def' a]; exact and_congr not_imp_not not_imp_notInformal description
For any decidable propositions $a$ and $b$, the equivalence $\neg a \leftrightarrow \neg b$ holds if and only if $a \leftrightarrow b$ holds.
Decidable.not_iff_comm
theorem
[Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a)
Full source
theorem Decidable.not_iff_comm [Decidable a] [Decidable b] : (¬a ↔ b) ↔ (¬b ↔ a) := by
rw [@iff_def (¬a), @iff_def (¬b)]; exact and_congr not_imp_comm imp_not_commInformal description
For any decidable propositions $a$ and $b$, the equivalence $\neg a \leftrightarrow b$ holds if and only if $\neg b \leftrightarrow a$ holds.
Decidable.not_iff
theorem
[Decidable b] : ¬(a ↔ b) ↔ (¬a ↔ b)
Informal description
For any decidable proposition $b$, the equivalence $\neg (a \leftrightarrow b)$ holds if and only if $\neg a \leftrightarrow b$ holds.
Decidable.iff_not_comm
theorem
[Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a)
Full source
theorem Decidable.iff_not_comm [Decidable a] [Decidable b] : (a ↔ ¬b) ↔ (b ↔ ¬a) := by
rw [@iff_def a, @iff_def b]; exact and_congr imp_not_comm not_imp_commInformal description
For any decidable propositions $a$ and $b$, the equivalence $a \leftrightarrow \neg b$ holds if and only if the equivalence $b \leftrightarrow \neg a$ holds.
Decidable.iff_iff_and_or_not_and_not
theorem
{a b : Prop} [Decidable b] : (a ↔ b) ↔ (a ∧ b) ∨ (¬a ∧ ¬b)
Informal description
For any propositions $a$ and $b$ with $b$ decidable, the equivalence $a \leftrightarrow b$ holds if and only if either both $a$ and $b$ are true, or both are false.
Decidable.iff_iff_not_or_and_or_not
theorem
[Decidable a] [Decidable b] : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
Full source
theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] :
(a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b) := by
rw [iff_iff_implies_and_implies (a := a) (b := b)]; simp only [imp_iff_not_or, Or.comm]Informal description
For any decidable propositions $a$ and $b$, the equivalence $a \leftrightarrow b$ holds if and only if both $(\neg a \lor b)$ and $(a \lor \neg b)$ hold.
Decidable.not_and_not_right
theorem
[Decidable b] : ¬(a ∧ ¬b) ↔ (a → b)
Informal description
For any proposition $a$ and decidable proposition $b$, the statement $\neg(a \land \neg b)$ is equivalent to the implication $a \to b$.
Decidable.not_and_iff_not_or_not
theorem
[Decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b
Informal description
For any decidable proposition $a$, the negation of the conjunction $a \land b$ is equivalent to the disjunction $\neg a \lor \neg b$, i.e., $\neg (a \land b) \leftrightarrow \neg a \lor \neg b$.
Decidable.not_and_iff_or_not_not
abbrev
Full source
@[deprecated Decidable.not_and_iff_not_or_not (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not := @Decidable.not_and_iff_not_or_notInformal description
For any decidable propositions $a$ and $b$, the negation of the conjunction $a \land b$ is equivalent to the disjunction $\neg a \lor \neg b$, i.e., $\neg (a \land b) \leftrightarrow \neg a \lor \neg b$.
Decidable.not_and_iff_not_or_not'
theorem
[Decidable b] : ¬(a ∧ b) ↔ ¬a ∨ ¬b
Informal description
For decidable propositions $a$ and $b$, the negation of the conjunction $a \land b$ is equivalent to the disjunction of the negations $\neg a \lor \neg b$.
Decidable.not_and_iff_or_not_not'
abbrev
Full source
@[deprecated Decidable.not_and_iff_not_or_not' (since := "2025-03-18")]
abbrev Decidable.not_and_iff_or_not_not' := @Decidable.not_and_iff_not_or_not'Informal description
For decidable propositions $a$ and $b$, the negation of the conjunction $a \land b$ is equivalent to the disjunction of the negations $\neg a \lor \neg b$.
Decidable.or_iff_not_not_and_not
theorem
[Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b)
Full source
theorem Decidable.or_iff_not_not_and_not [Decidable a] [Decidable b] : a ∨ ba ∨ b ↔ ¬(¬a ∧ ¬b) := by
rw [← not_or, not_not]Informal description
For any decidable propositions $a$ and $b$, the disjunction $a \lor b$ is equivalent to the negation of the conjunction of their negations, i.e., $a \lor b \leftrightarrow \neg(\neg a \land \neg b)$.
Decidable.or_iff_not_and_not
abbrev
Full source
@[deprecated Decidable.or_iff_not_not_and_not (since := "2025-03-18")]
abbrev Decidable.or_iff_not_and_not := @Decidable.or_iff_not_not_and_notInformal description
For any decidable propositions $a$ and $b$, the disjunction $a \lor b$ is equivalent to the negation of the conjunction of their negations, i.e., $a \lor b \leftrightarrow \neg(\neg a \land \neg b)$.
Decidable.and_iff_not_not_or_not
theorem
[Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b)
Full source
theorem Decidable.and_iff_not_not_or_not [Decidable a] [Decidable b] : a ∧ ba ∧ b ↔ ¬(¬a ∨ ¬b) := by
rw [← not_and_iff_not_or_not, not_not]Informal description
For any decidable propositions $a$ and $b$, the conjunction $a \land b$ is equivalent to the negation of $\neg a \lor \neg b$, i.e., $a \land b \leftrightarrow \neg(\neg a \lor \neg b)$.
Decidable.and_iff_not_or_not
abbrev
Full source
@[deprecated Decidable.and_iff_not_not_or_not (since := "2025-03-18")]
abbrev Decidable.and_iff_not_or_not := @Decidable.and_iff_not_not_or_notInformal description
For any decidable propositions $a$ and $b$, the conjunction $a \land b$ is equivalent to the negation of $\neg a \lor \neg b$, i.e., $a \land b \leftrightarrow \neg(\neg a \lor \neg b)$.
Decidable.imp_iff_right_iff
theorem
[Decidable a] : (a → b ↔ b) ↔ a ∨ b
Full source
theorem Decidable.imp_iff_right_iff [Decidable a] : (a → b ↔ b) ↔ a ∨ b :=
Iff.intro
(fun h => (Decidable.em a).imp_right fun ha' => h.mp fun ha => (ha' ha).elim)
(fun ab => ab.elim imp_iff_right fun hb => iff_of_true (fun _ => hb) hb)Informal description
For any decidable proposition $a$ and any proposition $b$, the equivalence $(a \to b) \leftrightarrow b$ holds if and only if $a \lor b$ holds.
Decidable.imp_iff_left_iff
theorem
[Decidable a] : (b ↔ a → b) ↔ a ∨ b
Full source
theorem Decidable.imp_iff_left_iff [Decidable a] : (b ↔ a → b) ↔ a ∨ b :=
propext (@Iff.comm (a → b) b) ▸ (@Decidable.imp_iff_right_iff a b _)Informal description
For any decidable proposition $a$ and any proposition $b$, the equivalence $b \leftrightarrow (a \to b)$ holds if and only if $a \lor b$ holds.
Decidable.and_or_imp
theorem
[Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ c
Informal description
For a decidable proposition $a$, the statement $(a \land b) \lor (a \to c)$ is equivalent to $a \to (b \lor c)$.
Decidable.or_congr_left'
theorem
[Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c
Full source
theorem Decidable.or_congr_left' [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ ca ∨ c ↔ b ∨ c := by
rw [or_iff_not_imp_right, or_iff_not_imp_right]; exact imp_congr_right hInformal description
For a decidable proposition $c$, if $\neg c$ implies that $a \leftrightarrow b$, then the disjunction $a \lor c$ holds if and only if $b \lor c$ holds.
Decidable.or_congr_right'
theorem
[Decidable a] (h : ¬a → (b ↔ c)) : a ∨ b ↔ a ∨ c
Full source
theorem Decidable.or_congr_right' [Decidable a] (h : ¬a → (b ↔ c)) : a ∨ ba ∨ b ↔ a ∨ c := by
rw [or_iff_not_imp_left, or_iff_not_imp_left]; exact imp_congr_right hInformal description
For a decidable proposition $a$, if $\neg a$ implies that $b \leftrightarrow c$, then $a \lor b$ holds if and only if $a \lor c$ holds.
Decidable.iff_congr_left
theorem
{P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] : ((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q)
Full source
@[simp] theorem Decidable.iff_congr_left {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
((P ↔ R) ↔ (Q ↔ R)) ↔ (P ↔ Q) :=
if h : R then by simp_all [Decidable.not_iff_not] else by simp_all [Decidable.not_iff_not]Informal description
For any propositions $P$, $Q$, and $R$ with decidable truth values, the equivalence $((P \leftrightarrow R) \leftrightarrow (Q \leftrightarrow R))$ holds if and only if $P \leftrightarrow Q$ holds.
Decidable.iff_congr_right
theorem
{P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] : ((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R)
Full source
@[simp] theorem Decidable.iff_congr_right {P Q R : Prop} [Decidable P] [Decidable Q] [Decidable R] :
((P ↔ Q) ↔ (P ↔ R)) ↔ (Q ↔ R) :=
if h : P then by simp_all [Decidable.not_iff_not] else by simp_all [Decidable.not_iff_not]Informal description
For any propositions $P$, $Q$, and $R$ (with decidability instances for each), the equivalence $((P \leftrightarrow Q) \leftrightarrow (P \leftrightarrow R))$ holds if and only if $Q \leftrightarrow R$ holds.
decidable_of_iff
definition
(a : Prop) (h : a ↔ b) [Decidable a] : Decidable b
Full source
/-- 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 `decide` will not work. -/
@[inline] def decidable_of_iff (a : Prop) (h : a ↔ b) [Decidable a] : Decidable b :=
decidable_of_decidable_of_iff hInformal description
Given two propositions $a$ and $b$ that are equivalent (i.e., $a \leftrightarrow b$), and a decision procedure for $a$, this function constructs a decision procedure for $b$.
decidable_of_iff'
definition
(b : Prop) (h : a ↔ b) [Decidable b] : Decidable a
Full source
/-- 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. -/
@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a :=
decidable_of_decidable_of_iff h.symmInformal description
Given two propositions $a$ and $b$ that are equivalent ($a \leftrightarrow b$), and given that $b$ is decidable, then $a$ is also decidable. This transfers the decidability from $b$ to $a$ via their logical equivalence.
Decidable.predToBool
instance
(p : α → Prop) [DecidablePred p] : CoeDep (α → Prop) p (α → Bool)
Full source
instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
CoeDep (α → Prop) p (α → Bool) := ⟨fun b => decide <| p b⟩Informal description
For any predicate `p : α → Prop` that is decidable, there exists a canonical coercion from `p` to a function `α → Bool` that represents the truth value of `p` for each input.
instDecidablePredComp
instance
[DecidablePred p] : DecidablePred (p ∘ f)
Full source
instance [DecidablePred p] : DecidablePred (p ∘ f) :=
fun x => inferInstanceAs (Decidable (p (f x)))Informal description
For any predicate `p` on a type `α` with a decidable truth value, the composition `p ∘ f` is also decidable for any function `f : β → α`.
decidable_of_bool
definition
: ∀ (b : Bool), (b ↔ a) → Decidable a
Full source
/-- 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.) -/
def decidable_of_bool : ∀ (b : Bool), (b ↔ a) → Decidable a
| true, h => isTrue (h.1 rfl)
| false, h => isFalse (mt h.2 Bool.noConfusion)Informal description
Given a boolean value \( b \) and a proof that \( b \) is equivalent to a proposition \( a \), this constructs a decision procedure for \( a \). Specifically:
- If \( b \) is true and \( b \leftrightarrow a \) holds, then \( a \) is true.
- If \( b \) is false and \( b \leftrightarrow a \) holds, then \( a \) is false.
This provides an alternative way to define decidability by constructing a boolean witness and its equivalence to the proposition.
Decidable.not_forall
theorem
{p : α → Prop} [Decidable (∃ x, ¬p x)] [∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x
Full source
protected theorem Decidable.not_forall {p : α → Prop} [Decidable (∃ x, ¬p x)]
[∀ x, Decidable (p x)] : (¬∀ x, p x) ↔ ∃ x, ¬p x :=
⟨Decidable.not_imp_symm fun nx x => Decidable.not_imp_symm (fun h => ⟨x, h⟩) nx,
not_forall_of_exists_not⟩Informal description
For any predicate $p$ on a type $\alpha$ where the existence of a counterexample $(\exists x, \neg p(x))$ is decidable and $p(x)$ is decidable for all $x \in \alpha$, the statement "not for all $x$, $p(x)$ holds" is equivalent to "there exists an $x$ such that $\neg p(x)$ holds". In symbols:
$$\neg (\forall x, p(x)) \leftrightarrow \exists x, \neg p(x)$$
Decidable.not_forall_not
theorem
{p : α → Prop} [Decidable (∃ x, p x)] : (¬∀ x, ¬p x) ↔ ∃ x, p x
Full source
protected theorem Decidable.not_forall_not {p : α → Prop} [Decidable (∃ x, p x)] :
(¬∀ x, ¬p x) ↔ ∃ x, p x :=
(@Decidable.not_iff_comm _ _ _ (decidable_of_iff (¬∃ x, p x) not_exists)).1 not_existsInformal description
For any predicate $p$ on a type $\alpha$ where the existence of an $x$ satisfying $p(x)$ is decidable, the statement "not for all $x$, $\neg p(x)$ holds" is equivalent to "there exists an $x$ such that $p(x)$ holds". In symbols:
$$\neg (\forall x, \neg p(x)) \leftrightarrow \exists x, p(x)$$
Decidable.not_exists_not
theorem
{p : α → Prop} [∀ x, Decidable (p x)] : (¬∃ x, ¬p x) ↔ ∀ x, p x
Full source
protected theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
(¬∃ x, ¬p x) ↔ ∀ x, p x := by
simp only [not_exists, Decidable.not_not]Informal description
For any predicate $p$ on a type $\alpha$ where $p(x)$ is decidable for all $x \in \alpha$, the statement "there does not exist an $x$ for which $p(x)$ is false" is equivalent to "for all $x$, $p(x)$ holds". In symbols:
$$\neg (\exists x, \neg p(x)) \leftrightarrow \forall x, p(x)$$
decide_implies
theorem
(u v : Prop) [duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v} :
decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true)
Full source
@[simp]
theorem decide_implies (u v : Prop)
[duv : Decidable (u → v)] [du : Decidable u] {dv : u → Decidable v}
: decide (u → v) = dite u (fun h => @decide v (dv h)) (fun _ => true) :=
if h : u then by
simp [h]
else by
simp [h]Informal description
For any propositions $u$ and $v$ with decidability instances for $u \to v$ and $u$, and given a function that provides a decidability instance for $v$ under the assumption $u$, the decision procedure for $u \to v$ is equal to the following: if $u$ holds, then use the decision procedure for $v$ (provided by the function), otherwise return true.
decide_ite
theorem
(u : Prop) [du : Decidable u] (p q : Prop) [dpq : Decidable (ite u p q)] [dp : Decidable p] [dq : Decidable q] :
decide (ite u p q) = ite u (decide p) (decide q)
Informal description
For any propositions $u$, $p$, and $q$ with decidable instances, the decision procedure for the if-then-else expression $\text{ite}(u, p, q)$ (which evaluates to $p$ if $u$ is true and $q$ otherwise) is equal to the if-then-else expression applied to the decision procedures for $p$ and $q$. That is,
\[
\text{decide}(\text{ite}(u, p, q)) = \text{ite}(u, \text{decide}(p), \text{decide}(q)).
\]
ite_then_decide_self
theorem
(p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) : (@ite _ p h (decide p) q) = (decide p || q)
Full source
@[simp] theorem ite_then_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
(@ite _ p h (decide p) q) = (decidedecide p || q) := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance `h`, and any boolean value $q$, the expression `if p then decide p else q` evaluates to the same boolean value as `decide p ∨ q`.
ite_else_decide_self
theorem
(p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) : (@ite _ p h q (decide p)) = (decide p && q)
Full source
@[simp] theorem ite_else_decide_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
(@ite _ p h q (decide p)) = (decidedecide p && q) := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance `h : Decidable p`, and for any boolean value $q$, the expression `if p then q else decide p` evaluates to the boolean conjunction of `decide p` and $q$, i.e., `decide p && q`.
ite_then_decide_not_self
theorem
(p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) : (@ite _ p h (!decide p) q) = (!decide p && q)
Full source
@[simp] theorem ite_then_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
(@ite _ p h (!decide p) q) = (!decide p!decide p && q) := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance, and any boolean $q$, the expression `if p then ¬(decide p) else q` evaluates to the same value as `¬(decide p) ∧ q`.
ite_else_decide_not_self
theorem
(p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) : (@ite _ p h q (!decide p)) = (!decide p || q)
Full source
@[simp] theorem ite_else_decide_not_self (p : Prop) [h : Decidable p] {w : Decidable p} (q : Bool) :
(@ite _ p h q (!decide p)) = (!decide p!decide p || q) := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance, and for any boolean $q$, the if-then-else expression `if p then q else ¬p` is equal to the boolean expression `¬p ∨ q`.
dite_eq_left_iff
theorem
{p : Prop} [Decidable p] {x : α} {y : ¬p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬p, y h = x
Full source
@[simp] theorem dite_eq_left_iff {p : Prop} [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance, an element $x$ of type $\alpha$, and a function $y$ from $\neg p$ to $\alpha$, the dependent if-then-else expression `(if h : p then x else y h)` equals $x$ if and only if for every proof $h$ of $\neg p$, the value $y h$ equals $x$.
dite_eq_right_iff
theorem
{p : Prop} [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y
Full source
@[simp] theorem dite_eq_right_iff {p : Prop} [Decidable p] {x : p → α} {y : α} : (if h : p then x h else y) = y ↔ ∀ h : p, x h = y := by
split <;> simp_allInformal description
For any proposition $p$ with a decidable instance, and for any function $x : p \to \alpha$ and element $y : \alpha$, the conditional expression `if h : p then x h else y` equals $y$ if and only if for every proof $h$ of $p$, the value $x h$ equals $y$.
dite_iff_left_iff
theorem
{p : Prop} [Decidable p] {x : Prop} {y : ¬p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬p, y h ↔ x
Full source
@[simp] theorem dite_iff_left_iff {p : Prop} [Decidable p] {x : Prop} {y : ¬ p → Prop} : ((if h : p then x else y h) ↔ x) ↔ ∀ h : ¬ p, y h ↔ x := by
split <;> simp_allInformal description
For a decidable proposition $p$ and propositions $x$ and $y(h)$ (where $y$ depends on $\neg p$), the equivalence $\left(\text{if } h : p \text{ then } x \text{ else } y(h)\right) \leftrightarrow x$ holds if and only if for all $h : \neg p$, $y(h) \leftrightarrow x$.
dite_iff_right_iff
theorem
{p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y
Full source
@[simp] theorem dite_iff_right_iff {p : Prop} [Decidable p] {x : p → Prop} {y : Prop} : ((if h : p then x h else y) ↔ y) ↔ ∀ h : p, x h ↔ y := by
split <;> simp_allInformal description
For any decidable proposition $p$, any family of propositions $x : p \to \mathrm{Prop}$, and any proposition $y$, the equivalence $\left(\text{if } h : p \text{ then } x h \text{ else } y\right) \leftrightarrow y$ holds if and only if for every proof $h$ of $p$, the proposition $x h$ is equivalent to $y$.
ite_eq_left_iff
theorem
{p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ↔ ¬p → y = x
Full source
@[simp] theorem ite_eq_left_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = x ↔ ¬ p → y = x := by
split <;> simp_allInformal description
For a decidable proposition $p$ and elements $x, y$ of a type $\alpha$, the equality $\text{if } p \text{ then } x \text{ else } y = x$ holds if and only if $\neg p$ implies $y = x$.
ite_eq_right_iff
theorem
{p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y
Full source
@[simp] theorem ite_eq_right_iff {p : Prop} [Decidable p] {x y : α} : (if p then x else y) = y ↔ p → x = y := by
split <;> simp_allInformal description
For any decidable proposition $p$ and elements $x, y$ of a type $\alpha$, the equality $\text{if } p \text{ then } x \text{ else } y = y$ holds if and only if $p$ implies $x = y$.
ite_iff_left_iff
theorem
{p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ x) ↔ ¬p → y = x
Full source
@[simp] theorem ite_iff_left_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ x) ↔ ¬ p → y = x := by
split <;> simp_allInformal description
For any decidable proposition $p$ and propositions $x$ and $y$, the equivalence $\left(\text{if } p \text{ then } x \text{ else } y\right) \leftrightarrow x$ holds if and only if $\neg p$ implies $y = x$.
ite_iff_right_iff
theorem
{p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y
Full source
@[simp] theorem ite_iff_right_iff {p : Prop} [Decidable p] {x y : Prop} : ((if p then x else y) ↔ y) ↔ p → x = y := by
split <;> simp_allInformal description
For any decidable proposition $p$ and propositions $x$ and $y$, the equivalence $\left((\text{if } p \text{ then } x \text{ else } y) \leftrightarrow y\right)$ holds if and only if $p$ implies $x = y$.
dite_then_false
theorem
{p : Prop} [Decidable p] {x : ¬p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬p, x h
Full source
@[simp] theorem dite_then_false {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h := by
split <;> simp_allInformal description
For any decidable proposition $p$ and any predicate $x$ on $\neg p$, the statement "if $p$ holds then `False` else $x(h)$ for $h : \neg p$" is equivalent to "there exists $h : \neg p$ such that $x(h)$ holds".
In symbols:
$$
(\text{if } h : p \text{ then } \text{False} \text{ else } x(h)) \leftrightarrow (\exists h : \neg p, x(h))
$$
dite_else_false
theorem
{p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ h : p, x h
Full source
@[simp] theorem dite_else_false {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else False) ↔ ∃ h : p, x h := by
split <;> simp_allInformal description
For any decidable proposition $p$ and any predicate $x$ on $p$, the statement "if $h : p$ then $x(h)$ else false" is equivalent to "there exists $h : p$ such that $x(h)$ holds". In other words:
$$\left(\text{if } h : p \text{ then } x(h) \text{ else } \text{False}\right) \leftrightarrow \left(\exists h : p, x(h)\right)$$
dite_then_true
theorem
{p : Prop} [Decidable p] {x : ¬p → Prop} : (if h : p then True else x h) ↔ ∀ h : ¬p, x h
Full source
@[simp] theorem dite_then_true {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then True else x h) ↔ ∀ h : ¬ p, x h := by
split <;> simp_allInformal description
For any decidable proposition $p$ and any predicate $x$ on $\neg p$, the statement "if $p$ holds then `True` else $x(h)$ for $h : \neg p$" is equivalent to "for all $h : \neg p$, $x(h)$ holds".
In symbols:
$$
(\text{if } h : p \text{ then } \text{True} \text{ else } x(h)) \leftrightarrow (\forall h : \neg p, x(h))
$$
dite_else_true
theorem
{p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ h : p, x h
Full source
@[simp] theorem dite_else_true {p : Prop} [Decidable p] {x : p → Prop} : (if h : p then x h else True) ↔ ∀ h : p, x h := by
split <;> simp_allInformal description
For any decidable proposition $p$ and any predicate $x$ on $p$, the statement "if $h : p$ then $x(h)$ else true" is equivalent to "for all $h : p$, $x(h)$ holds". In other words:
$$\left(\text{if } h : p \text{ then } x(h) \text{ else } \text{True}\right) \leftrightarrow \left(\forall h : p, x(h)\right)$$