Init.Classical

Classical.indefiniteDescription definition

{α : Sort u} (p : α → Prop) (h : ∃ x, p x) : { x // p x }

Full source

noncomputable def indefiniteDescription {α : Sort u} (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
  choice <| let ⟨x, px⟩ := h; ⟨⟨x, px⟩⟩

Existence of indefinite description

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ such that $p(x)$ holds, then there exists a term of the subtype $\{x \mid p(x)\}$.

Classical.choose definition

{α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α

Full source

/--
Given that there exists an element satisfying `p`, returns one such element.

This is a straightforward consequence of, and equivalent to, `Classical.choice`.

See also `choose_spec`, which asserts that the returned value has property `p`.
-/
noncomputable def choose {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : α :=
  (indefiniteDescription p h).val

Choice function for existential statements

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ such that $p(x)$ holds, then this function returns one such element. This is equivalent to the axiom of choice.

Classical.choose_spec theorem

{α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h)

Full source

theorem choose_spec {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : p (choose h) :=
  (indefiniteDescription p h).property

Property of the Chosen Element in the Axiom of Choice

Informal description

For any type $\alpha$ and predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ such that $p(x)$ holds, then the element chosen by `Classical.choose` satisfies $p$. That is, $p(\text{choose}(h))$ holds where $h$ is the proof of $\exists x, p(x)$.

Classical.em theorem

(p : Prop) : p ∨ ¬p

Full source

/-- **Diaconescu's theorem**: excluded middle from choice, Function extensionality and propositional extensionality. -/
theorem em (p : Prop) : p ∨ ¬p :=
  let U (x : Prop) : Prop := x = True ∨ p
  let V (x : Prop) : Prop := x = False ∨ p
  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
  let u : Prop := choose exU
  let v : Prop := choose exV
  have u_def : U u := choose_spec exU
  have v_def : V v := choose_spec exV
  have not_uv_or_p : u ≠ vu ≠ v ∨ p :=
    match u_def, v_def with
    | Or.inr h, _ => Or.inr h
    | _, Or.inr h => Or.inr h
    | Or.inl hut, Or.inl hvf =>
      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
      Or.inl hne
  have p_implies_uv : p → u = v :=
    fun hp =>
    have hpred : U = V :=
      funext fun x =>
        have hl : (x = True ∨ p) → (x = False ∨ p) :=
          fun _ => Or.inr hp
        have hr : (x = False ∨ p) → (x = True ∨ p) :=
          fun _ => Or.inr hp
        show (x = True ∨ p) = (x = False ∨ p) from
          propext (Iff.intro hl hr)
    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
      rw [hpred]; intros; rfl
    show u = v from h₀ _ _
  match not_uv_or_p with
  | Or.inl hne => Or.inr (mt p_implies_uv hne)
  | Or.inr h   => Or.inl h

Law of the Excluded Middle

Informal description

For any proposition $p$, either $p$ holds or its negation $\neg p$ holds.

Classical.exists_true_of_nonempty theorem

{α : Sort u} : Nonempty α → ∃ _ : α, True

Full source

theorem exists_true_of_nonempty {α : Sort u} : Nonempty α → ∃ _ : α, True
  | ⟨x⟩ => ⟨x, trivial⟩

Existence of Element in Nonempty Type

Informal description

For any nonempty type $\alpha$, there exists an element of $\alpha$ for which the proposition `True` holds.

Classical.inhabited_of_nonempty definition

{α : Sort u} (h : Nonempty α) : Inhabited α

Full source

noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabited α :=
  ⟨choice h⟩

Construction of inhabited type from nonempty type

Informal description

Given a nonempty type $\alpha$, this function constructs an instance of `Inhabited α` by selecting an arbitrary element of $\alpha$ using the axiom of choice.

Classical.inhabited_of_exists definition

{α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α

Full source

noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α :=
  inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩))

Inhabited type from existence proof

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if there exists an element $x$ in $\alpha$ satisfying $p(x)$, then $\alpha$ is inhabited (i.e., there exists at least one element in $\alpha$).

Classical.propDecidable instance

(a : Prop) : Decidable a

Full source

/-- All propositions are `Decidable`. -/
noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
  choice <| match em a with
    | Or.inl h => ⟨isTrue h⟩
    | Or.inr h => ⟨isFalse h⟩

Decidability of All Propositions in Classical Logic

Informal description

Every proposition is decidable under classical logic.

Classical.decidableInhabited definition

(a : Prop) : Inhabited (Decidable a)

Full source

noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) where
  default := inferInstance

Inhabited decidability of propositions in classical logic

Informal description

For any proposition $ a $, the type `Decidable a` is inhabited, meaning there exists a default instance that can decide $ a $ under classical logic.

Classical.instNonemptyDecidable instance

(a : Prop) : Nonempty (Decidable a)

Full source

instance (a : Prop) : Nonempty (Decidable a) := ⟨propDecidable a⟩

Existence of Decidable Instances for Propositions in Classical Logic

Informal description

For any proposition $a$, there exists a decidable instance for $a$ under classical logic.

Classical.typeDecidableEq definition

(α : Sort u) : DecidableEq α

Full source

noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
  fun _ _ => inferInstance

Decidable equality in classical logic

Informal description

For any type `α`, the equality relation on `α` is decidable under classical logic.

Classical.typeDecidable definition

(α : Sort u) : PSum α (α → False)

Full source

noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) :=
  match (propDecidable (Nonempty α)) with
  | (isTrue hp)  => PSum.inl (@default _ (inhabited_of_nonempty hp))
  | (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn)

Decidability of type inhabitation

Informal description

Given a type $\alpha$, this function decides whether $\alpha$ is inhabited or empty, returning either an element of $\alpha$ or a proof that $\alpha$ is empty.

Classical.strongIndefiniteDescription definition

{α : Sort u} (p : α → Prop) (h : Nonempty α) : { x : α // (∃ y : α, p y) → p x }

Full source

noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // (∃ y : α, p y) → p x} :=
  @dite _ (∃ x : α, p x) (propDecidable _)
    (fun (hp : ∃ x : α, p x) =>
      show {x : α // (∃ y : α, p y) → p x} from
      let xp := indefiniteDescription _ hp;
      ⟨xp.val, fun _ => xp.property⟩)
    (fun hp => ⟨choice h, fun h => absurd h hp⟩)

Strong indefinite description principle

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if $\alpha$ is nonempty, then there exists an element $x$ in $\alpha$ such that if there exists any $y$ in $\alpha$ satisfying $p(y)$, then $x$ satisfies $p(x)$. This is a stronger version of the indefinite description principle that guarantees the existence of a witness under weaker conditions.

Classical.epsilon definition

{α : Sort u} [h : Nonempty α] (p : α → Prop) : α

Full source

/-- the Hilbert epsilon Function -/
noncomputable def epsilon {α : Sort u} [h : Nonempty α] (p : α → Prop) : α :=
  (strongIndefiniteDescription p h).val

Hilbert epsilon function

Informal description

The Hilbert choice function $\epsilon$ takes a nonempty type $\alpha$ and a predicate $p$ on $\alpha$, and returns an element of $\alpha$ such that if there exists any $y$ in $\alpha$ satisfying $p(y)$, then $\epsilon p$ satisfies $p(\epsilon p)$. More formally, given a nonempty type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$, $\epsilon p$ is an element of $\alpha$ with the property that $(\exists y, p y) \to p(\epsilon p)$.

Classical.epsilon_spec_aux theorem

{α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p)

Full source

theorem epsilon_spec_aux {α : Sort u} (h : Nonempty α) (p : α → Prop) : (∃ y, p y) → p (@epsilon α h p) :=
  (strongIndefiniteDescription p h).property

Hilbert Epsilon Property: $(\exists y, p(y)) \rightarrow p(\epsilon p)$

Informal description

For any nonempty type $\alpha$ and predicate $p$ on $\alpha$, if there exists some $y \in \alpha$ satisfying $p(y)$, then the Hilbert choice function $\epsilon p$ satisfies $p(\epsilon p)$.

Classical.epsilon_spec theorem

{α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p)

Full source

theorem epsilon_spec {α : Sort u} {p : α → Prop} (hex : ∃ y, p y) : p (@epsilon α (nonempty_of_exists hex) p) :=
  epsilon_spec_aux (nonempty_of_exists hex) p hex

Hilbert Epsilon Property: $(\exists y, p(y)) \rightarrow p(\epsilon p)$

Informal description

For any type $\alpha$ and predicate $p$ on $\alpha$, if there exists an element $y \in \alpha$ satisfying $p(y)$, then the Hilbert choice function $\epsilon p$ satisfies $p(\epsilon p)$.

Classical.epsilon_singleton theorem

{α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x

Full source

theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (fun y => y = x) = x :=
  @epsilon_spec α (fun y => y = x) ⟨x, rfl⟩

Hilbert Epsilon Selects Singleton: $\epsilon (y = x) = x$

Informal description

For any type $\alpha$ and element $x \in \alpha$, the Hilbert choice function $\epsilon$ applied to the predicate $y \mapsto y = x$ (with the nonempty instance provided by $\langle x \rangle$) returns $x$ itself, i.e., $\epsilon (y \mapsto y = x) = x$.

Classical.axiomOfChoice theorem

 {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x)

Full source

/-- the axiom of choice -/
theorem axiomOfChoice {α : Sort u} {β : α → Sort v} {r : ∀ x, β x → Prop} (h : ∀ x, ∃ y, r x y) : ∃ (f : ∀ x, β x), ∀ x, r x (f x) :=
  ⟨_, fun x => choose_spec (h x)⟩

Axiom of Choice for Dependent Types

Informal description

For any family of types $\beta$ indexed by $\alpha$ and a relation $r$ on each $\beta(x)$, if for every $x \in \alpha$ there exists $y \in \beta(x)$ such that $r(x, y)$ holds, then there exists a choice function $f \colon \prod_{x \in \alpha} \beta(x)$ such that for every $x \in \alpha$, the relation $r(x, f(x))$ holds.

Classical.skolem theorem

 {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, ∃ y, p x y) ↔ ∃ (f : ∀ x, b x), ∀ x, p x (f x)

Full source

theorem skolem {α : Sort u} {b : α → Sort v} {p : ∀ x, b x → Prop} : (∀ x, ∃ y, p x y) ↔ ∃ (f : ∀ x, b x), ∀ x, p x (f x) :=
  ⟨axiomOfChoice, fun ⟨f, hw⟩ (x) => ⟨f x, hw x⟩⟩

Skolem's Theorem: Universal-Existential Equivalence via Choice Function

Informal description

For any family of types $\beta$ indexed by $\alpha$ and a predicate $p$ on each $\beta(x)$, the statement $(\forall x, \exists y, p(x, y))$ is equivalent to the existence of a function $f \colon \prod_{x \in \alpha} \beta(x)$ such that $\forall x, p(x, f(x))$.

Classical.propComplete theorem

(a : Prop) : a = True ∨ a = False

Full source

theorem propComplete (a : Prop) : a = True ∨ a = False :=
  match em a with
  | Or.inl ha => Or.inl (eq_true ha)
  | Or.inr hn => Or.inr (eq_false hn)

Propositional Completeness in Classical Logic

Informal description

For any proposition $a$, either $a$ is equal to the true proposition $\text{True}$ or $a$ is equal to the false proposition $\text{False}$.

Classical.byCases theorem

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

Full source

theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
  Decidable.byCases (dec := propDecidable _) hpq hnpq

Proof by Cases in Classical Logic

Informal description

For any propositions $p$ and $q$, if $p$ implies $q$ and $\neg p$ also implies $q$, then $q$ holds.

Classical.byContradiction theorem

{p : Prop} (h : ¬p → False) : p

Full source

theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
  Decidable.byContradiction (dec := propDecidable _) h

Proof by Contradiction

Informal description

For any proposition $p$, if assuming $\neg p$ leads to a contradiction, then $p$ holds.

Classical.not_not theorem

: ¬¬a ↔ a

Full source

/-- The Double Negation Theorem: `¬¬P` is equivalent to `P`.
The left-to-right direction, double negation elimination (DNE),
is classically true but not constructively. -/
@[simp] theorem not_not : ¬¬a¬¬a ↔ a := Decidable.not_not

Double Negation Theorem: $\neg \neg P \leftrightarrow P$

Informal description

For any proposition $P$, the double negation $\neg \neg P$ is equivalent to $P$.

Classical.decidable_of_decidable_not definition

(p : Prop) [h : Decidable (¬p)] : Decidable p

Full source

/-- Transfer decidability of `¬ p` to decidability of `p`. -/
-- This can not be an instance as it would be tried everywhere.
def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
  match h with
  | isFalse h => isTrue (Classical.not_not.mp h)
  | isTrue h => isFalse h

Decidability transfer from negation

Informal description

Given a proposition $ p $, if the decidability of $ \neg p $ is known, then the decidability of $ p $ can be inferred. Specifically: - If $ \neg p $ is false (i.e., $ \neg p $ is not provable), then $ p $ is true. - If $ \neg p $ is true (i.e., $ \neg p $ is provable), then $ p $ is false. This definition transfers the decidability of the negation of a proposition to the proposition itself.

Classical.dite_not theorem

[hn : Decidable (¬p)] (x : ¬p → α) (y : ¬¬p → α) : dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x

Full source

/-- Negation of the condition `P : Prop` in a `dite` is the same as swapping the branches. -/
@[simp low] protected theorem dite_not [hn : Decidable (¬p)] (x : ¬p → α) (y : ¬¬p → α) :
    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x := by
  cases hn <;> rename_i g
  · simp [not_not.mp g]
  · simp [g]

Negation Swaps Branches in Dependent Conditional Expression

Informal description

For any proposition $p$ with decidable negation, and for any functions $x : \neg p \to \alpha$ and $y : \neg \neg p \to \alpha$, the dependent if-then-else expression $\text{dite}(\neg p, x, y)$ is equal to $\text{dite}(p, \lambda h, y(\neg\neg h), x)$. In other words, the negation of the condition in a dependent if-then-else expression is equivalent to swapping the branches and wrapping the positive case with double negation elimination.

Classical.ite_not theorem

(p : Prop) [Decidable (¬p)] (x y : α) : ite (¬p) x y = ite p y x

Full source

/-- Negation of the condition `P : Prop` in a `ite` is the same as swapping the branches. -/
@[simp low] protected theorem ite_not (p : Prop) [Decidable (¬ p)] (x y : α) : ite (¬p) x y = ite p y x :=
  dite_not (fun _ => x) (fun _ => y)

Negation Swaps Branches in Conditional Expression

Informal description

For any proposition $p$ and any elements $x, y$ of type $\alpha$, if the decidability of $\neg p$ is known, then the conditional expression $\text{ite}(\neg p, x, y)$ is equal to $\text{ite}(p, y, x)$. In other words, the negation of the condition in an if-then-else expression is equivalent to swapping the branches of the expression.

Classical.decide_not theorem

(p : Prop) [Decidable (¬p)] : decide (¬p) = !decide p

Full source

@[simp low] protected theorem decide_not (p : Prop) [Decidable (¬ p)] : decide (¬p) = !decide p :=
  byCases (fun h : p => by simp_all) (fun h => by simp_all)

Negation of Decision Procedure for Proposition $p$

Informal description

For any proposition $p$ with a decidable negation, the decision procedure for $\neg p$ is equivalent to the negation of the decision procedure for $p$, i.e., $\text{decide}(\neg p) = \neg \text{decide}(p)$.

Classical.not_forall theorem

{p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x

Full source

@[simp low] theorem not_forall {p : α → Prop} : (¬∀ x, p x) ↔ ∃ x, ¬p x := Decidable.not_forall

Negation of Universal Quantifier is Existential Quantifier of Negation

Informal description

For any predicate $p$ on a type $\alpha$, the negation of the universal statement $\forall x, p(x)$ is equivalent to the existence of a counterexample, i.e., $\neg (\forall x, p(x)) \leftrightarrow \exists x, \neg p(x)$.

Classical.not_forall_not theorem

{p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x

Full source

theorem not_forall_not {p : α → Prop} : (¬∀ x, ¬p x) ↔ ∃ x, p x := Decidable.not_forall_not

Double Negation of Universal Quantifier is Equivalent to Existential Quantifier

Informal description

For any predicate $p$ on a type $\alpha$, the statement "it is not the case that for all $x$, $p(x)$ does not hold" 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) $$

Classical.not_exists_not theorem

{p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x

Full source

theorem not_exists_not {p : α → Prop} : (¬∃ x, ¬p x) ↔ ∀ x, p x := Decidable.not_exists_not

Double Negation in Quantifiers: $\neg \exists \neg p \leftrightarrow \forall p$

Informal description

For any predicate $p$ on a type $\alpha$, the statement "there does not exist an $x$ such that $\neg p(x)$" is equivalent to "for all $x$, $p(x)$ holds." In symbols: $$ \neg (\exists x, \neg p(x)) \leftrightarrow \forall x, p(x). $$

Classical.forall_or_exists_not theorem

(P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬P a

Full source

theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a := by
  rw [← not_forall]; exact em _

Universal Quantifier or Existential Negation: $(\forall a, P(a)) \lor (\exists a, \neg P(a))$

Informal description

For any predicate $P$ on a type $\alpha$, either $P(a)$ holds for all $a \in \alpha$, or there exists some $a \in \alpha$ for which $\neg P(a)$ holds.

Classical.exists_or_forall_not theorem

(P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬P a

Full source

theorem exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a := by
  rw [← not_exists]; exact em _

Existential or Universal Negation: $(\exists a, P(a)) \lor (\forall a, \neg P(a))$

Informal description

For any predicate $P$ on a type $\alpha$, either there exists an element $a \in \alpha$ such that $P(a)$ holds, or for all $a \in \alpha$, $\neg P(a)$ holds.

Classical.or_iff_not_imp_left theorem

: a ∨ b ↔ (¬a → b)

Full source

theorem or_iff_not_imp_left  : a ∨ ba ∨ b ↔ (¬a → b) := Decidable.or_iff_not_imp_left

Disjunction Equivalence: $a \lor b \leftrightarrow (\neg a \to b)$

Informal description

For any propositions $a$ and $b$, the disjunction $a \lor b$ holds if and only if the implication $\neg a \to b$ holds.

Classical.or_iff_not_imp_right theorem

: a ∨ b ↔ (¬b → a)

Full source

theorem or_iff_not_imp_right : a ∨ ba ∨ b ↔ (¬b → a) := Decidable.or_iff_not_imp_right

Disjunction Equivalence: $a \lor b \leftrightarrow (\neg b \to a)$

Informal description

For any propositions $a$ and $b$, the disjunction $a \lor b$ holds if and only if the implication $\neg b \to a$ holds.

Classical.not_imp_iff_and_not theorem

: ¬(a → b) ↔ a ∧ ¬b

Full source

theorem not_imp_iff_and_not : ¬(a → b)¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not

Negation of Implication is Conjunction of Antecedent and Negation of Consequent

Informal description

For any propositions $a$ and $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)$.

Classical.not_and_iff_not_or_not theorem

: ¬(a ∧ b) ↔ ¬a ∨ ¬b

Full source

theorem not_and_iff_not_or_not : ¬(a ∧ b)¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not

De Morgan's Law for Conjunction and Disjunction

Informal description

For any propositions $a$ and $b$, the negation of their conjunction is equivalent to the disjunction of their negations, i.e., $\neg(a \land b) \leftrightarrow \neg a \lor \neg b$.

Classical.not_and_iff_or_not_not abbrev

Full source

@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not

De Morgan's Law with Double Negation: $\neg(a \land b) \leftrightarrow \neg a \lor \neg\neg b$

Informal description

For any propositions $a$ and $b$, the negation of their conjunction is equivalent to the disjunction of the negation of $a$ and the double negation of $b$, i.e., $\neg(a \land b) \leftrightarrow \neg a \lor \neg\neg b$.

Classical.not_iff theorem

: ¬(a ↔ b) ↔ (¬a ↔ b)

Full source

theorem not_iff : ¬(a ↔ b)¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff

Negation of Biconditional: $\neg (a \leftrightarrow b) \leftrightarrow (\neg a \leftrightarrow b)$

Informal description

For any propositions $a$ and $b$, the negation of their biconditional is equivalent to the biconditional of the negation of $a$ and $b$, i.e., $\neg (a \leftrightarrow b) \leftrightarrow (\neg a \leftrightarrow b)$.

Classical.imp_iff_left_iff theorem

: (b ↔ a → b) ↔ a ∨ b

Full source

@[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff

Implication Equivalence: $(b \leftrightarrow (a \rightarrow b)) \leftrightarrow a \lor b$

Informal description

For any propositions $a$ and $b$, the equivalence $(b \leftrightarrow (a \rightarrow b))$ holds if and only if $a \lor b$ holds.

Classical.imp_iff_right_iff theorem

: (a → b ↔ b) ↔ a ∨ b

Full source

@[simp] theorem imp_iff_right_iff : (a → b ↔ b) ↔ a ∨ b := Decidable.imp_iff_right_iff

Implication Equivalence: $(a \to b \leftrightarrow b) \leftrightarrow (a \lor b)$

Informal description

For any propositions $a$ and $b$, the equivalence $(a \to b) \leftrightarrow b$ holds if and only if $a \lor b$ holds.

Classical.and_or_imp theorem

: a ∧ b ∨ (a → c) ↔ a → b ∨ c

Full source

@[simp] theorem and_or_imp : a ∧ ba ∧ b ∨ (a → c)a ∧ b ∨ (a → c) ↔ a → b ∨ c := Decidable.and_or_imp

Disjunction of Conjunction and Implication Equivalence

Informal description

For any propositions $a$, $b$, and $c$, the statement $(a \land b) \lor (a \to c)$ is equivalent to $a \to (b \lor c)$.

Classical.not_imp theorem

: ¬(a → b) ↔ a ∧ ¬b

Full source

@[simp] theorem not_imp : ¬(a → b)¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff_and_not

Negation of Implication Equivalence: $\neg(a \to b) \leftrightarrow (a \land \neg b)$

Informal description

For any propositions $a$ and $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)$.

Classical.imp_and_neg_imp_iff theorem

(p : Prop) {q : Prop} : (p → q) ∧ (¬p → q) ↔ q

Full source

@[simp] theorem imp_and_neg_imp_iff (p : Prop) {q : Prop} : (p → q) ∧ (¬p → q)(p → q) ∧ (¬p → q) ↔ q :=
  Iff.intro (fun (a : _ ∧ _) => (Classical.em p).rec a.left a.right)
            (fun a => And.intro (fun _ => a) (fun _ => a))

Implication and Negated Implication Equivalence: $(p \to q) \land (\neg p \to q) \leftrightarrow q$

Informal description

For any propositions $p$ and $q$, the conjunction $(p \to q) \land (\neg p \to q)$ is equivalent to $q$.

Exists.choose definition

{p : α → Prop} (P : ∃ a, p a) : α

Full source

/-- Extract an element from an existential statement, using `Classical.choose`. -/
-- This enables projection notation.
@[reducible] noncomputable def Exists.choose {p : α → Prop} (P : ∃ a, p a) : α := Classical.choose P

Choice function for existential statements

Informal description

Given a type $\alpha$ and a predicate $p$ on $\alpha$, if there exists an element $a$ in $\alpha$ such that $p(a)$ holds, then this function returns one such element. This is equivalent to the axiom of choice.

Exists.choose_spec theorem

{p : α → Prop} (P : ∃ a, p a) : p P.choose

Full source

/-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P

Property of the Chosen Element in an Existential Statement

Informal description

For any type $\alpha$ and predicate $p$ on $\alpha$, if there exists an element $a$ in $\alpha$ such that $p(a)$ holds, then the element $P.\text{choose}$ (where $P$ is the proof of $\exists a, p(a)$) satisfies $p$. That is, $p(P.\text{choose})$ holds.