Documentation

Mathlib.Logic.Basic

Basic logic properties #

This file is one of the earliest imports in mathlib.

Implementation notes #

Theorems that require decidability hypotheses are in the namespace Decidable. Classical versions are in the namespace Classical.

@[reducible]
def hidden {α : Sort u_1} {a : α} :
α

An identity function with its main argument implicit. This will be printed as hidden even if it is applied to a large term, so it can be used for elision, as done in the elide and unelide tactics.

Equations
  • hidden = a
Instances For
    instance instSubsingletonSubtype (α : Sort u_1) [Subsingleton α] (p : αProp) :
    Equations
    • =
    theorem congr_heq {α : Sort u_1} {β : Sort u_1} {γ : Sort u_2} {f : αγ} {g : βγ} {x : α} {y : β} (h₁ : HEq f g) (h₂ : HEq x y) :
    f x = g y
    theorem congr_arg_heq {α : Sort u_2} {β : αSort u_1} (f : (a : α) → β a) {a₁ : α} {a₂ : α} :
    a₁ = a₂HEq (f a₁) (f a₂)
    theorem ULift.down_injective {α : Type u_1} :
    @[simp]
    theorem ULift.down_inj {α : Type u_1} {a : ULift.{u_2, u_1} α} {b : ULift.{u_2, u_1} α} :
    a.down = b.down a = b
    theorem PLift.down_injective {α : Sort u_1} :
    @[simp]
    theorem PLift.down_inj {α : Sort u_1} {a : PLift α} {b : PLift α} :
    a.down = b.down a = b
    @[simp]
    theorem eq_iff_eq_cancel_left {α : Sort u_1} {b : α} {c : α} :
    (∀ {a : α}, a = b a = c) b = c
    @[simp]
    theorem eq_iff_eq_cancel_right {α : Sort u_1} {a : α} {b : α} :
    (∀ {c : α}, a = c b = c) a = b
    theorem ne_and_eq_iff_right {α : Sort u_1} {a : α} {b : α} {c : α} (h : b c) :
    a b a = c a = c
    class Fact (p : Prop) :

    Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details.

    Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances.

    For example, ZMod p is a field if and only if p is a prime number. In order to be able to find this field instance automatically by type class search, we have to turn p.prime into an instance implicit assumption.

    On the other hand, making Nat.prime a class would require a major refactoring of the library, and it is questionable whether making Nat.prime a class is desirable at all. The compromise is to add the assumption [Fact p.prime] to ZMod.field.

    In particular, this class is not intended for turning the type class system into an automated theorem prover for first order logic.

    • out : p

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

    Instances
      theorem Fact.elim {p : Prop} (h : Fact p) :
      p
      theorem fact_iff {p : Prop} :
      Fact p p
      @[reducible]
      def Function.swap₂ {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁Sort u_1} {κ₂ : ι₂Sort u_2} {φ : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Sort u_3} (f : (i₁ : ι₁) → (j₁ : κ₁ i₁) → (i₂ : ι₂) → (j₂ : κ₂ i₂) → φ i₁ j₁ i₂ j₂) (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁) :
      φ i₁ j₁ i₂ j₂

      Swaps two pairs of arguments to a function.

      Equations
      Instances For

        Declarations about propositional connectives #

        Declarations about implies #

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

        Alias of imp_congr.

        @[simp]
        theorem eq_true_eq_id :
        Eq True = id
        @[simp]
        theorem imp_iff_right_iff {a : Prop} {b : Prop} :
        (ab b) a b
        @[simp]
        theorem and_or_imp {a : Prop} {b : Prop} {c : Prop} :
        a b (ac) ab c
        theorem Function.mt {a : Prop} {b : Prop} :
        (ab)¬b¬a

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

        Declarations about not #

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

        Alias of Decidable.em.

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

        Alias of Classical.em.


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

        theorem em' (p : Prop) :
        ¬p p
        theorem or_not {p : Prop} :
        p ¬p
        theorem Decidable.eq_or_ne {α : Sort u_1} (x : α) (y : α) [Decidable (x = y)] :
        x = y x y
        theorem Decidable.ne_or_eq {α : Sort u_1} (x : α) (y : α) [Decidable (x = y)] :
        x y x = y
        theorem eq_or_ne {α : Sort u_1} (x : α) (y : α) :
        x = y x y
        theorem ne_or_eq {α : Sort u_1} (x : α) (y : α) :
        x y x = y
        theorem by_contradiction {p : Prop} :
        (¬pFalse)p
        theorem by_cases {p : Prop} {q : Prop} (hpq : pq) (hnpq : ¬pq) :
        q
        theorem by_contra {p : Prop} :
        (¬pFalse)p

        Alias of by_contradiction.

        theorem of_not_not {a : Prop} :
        ¬¬aa
        theorem not_ne_iff :
        ∀ {α : Sort u_1} {a b : α}, ¬a b a = b
        theorem of_not_imp {a : Prop} {b : Prop} :
        ¬(ab)a
        theorem Not.decidable_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬ab) (hb : ¬b) :
        a

        Alias of Decidable.not_imp_symm.

        theorem Not.imp_symm {a : Prop} {b : Prop} :
        (¬ab)¬ba
        theorem not_imp_comm {a : Prop} {b : Prop} :
        ¬ab ¬ba
        @[simp]
        theorem not_imp_self {a : Prop} :
        ¬aa a
        theorem Imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} :
        abc bac
        theorem Iff.not {a : Prop} {b : Prop} (h : a b) :

        Alias of not_congr.

        theorem Iff.not_left {a : Prop} {b : Prop} (h : a ¬b) :
        ¬a b
        theorem Iff.not_right {a : Prop} {b : Prop} (h : ¬a b) :
        a ¬b
        theorem Iff.ne {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a = b c = d)(a b c d)
        theorem Iff.ne_left {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a = b c d)(a b c = d)
        theorem Iff.ne_right {α : Sort u_1} {β : Sort u_2} {a : α} {b : α} {c : β} {d : β} :
        (a b c = d)(a = b c d)

        Declarations about Xor' #

        @[simp]
        @[simp]
        theorem xor_false :
        theorem xor_comm (a : Prop) (b : Prop) :
        Xor' a b = Xor' b a
        @[simp]
        theorem xor_self (a : Prop) :
        @[simp]
        theorem xor_not_left {a : Prop} {b : Prop} :
        Xor' (¬a) b (a b)
        @[simp]
        theorem xor_not_right {a : Prop} {b : Prop} :
        Xor' a ¬b (a b)
        theorem xor_not_not {a : Prop} {b : Prop} :
        Xor' (¬a) ¬b Xor' a b
        theorem Xor'.or {a : Prop} {b : Prop} (h : Xor' a b) :
        a b

        Declarations about and #

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

        Alias of and_congr.

        theorem And.rotate {a : Prop} {b : Prop} {c : Prop} :
        a b cb c a

        Alias of the forward direction of and_rotate.

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

        Declarations about or #

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

        Alias of or_congr.

        theorem Or.rotate {a : Prop} {b : Prop} {c : Prop} :
        a b cb c a

        Alias of the forward direction of or_rotate.

        @[deprecated Or.imp]
        theorem or_of_or_of_imp_of_imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₁ : a b) (h₂ : ac) (h₃ : bd) :
        c d
        @[deprecated Or.imp_left]
        theorem or_of_or_of_imp_left {a : Prop} {c : Prop} {b : Prop} (h₁ : a c) (h : ab) :
        b c
        @[deprecated Or.imp_right]
        theorem or_of_or_of_imp_right {c : Prop} {a : Prop} {b : Prop} (h₁ : c a) (h : ab) :
        c b
        theorem Or.elim3 {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h : a b c) (ha : ad) (hb : bd) (hc : cd) :
        d
        theorem Or.imp3 {a : Prop} {d : Prop} {b : Prop} {e : Prop} {c : Prop} {f : Prop} (had : ad) (hbe : be) (hcf : cf) :
        a b cd e f
        theorem not_or_of_imp {a : Prop} {b : Prop} :
        (ab)¬a b
        theorem Decidable.or_not_of_imp {a : Prop} {b : Prop} [Decidable a] (h : ab) :
        b ¬a
        theorem or_not_of_imp {a : Prop} {b : Prop} :
        (ab)b ¬a
        theorem imp_iff_not_or {a : Prop} {b : Prop} :
        ab ¬a b
        theorem imp_iff_or_not {b : Prop} {a : Prop} :
        ba a ¬b
        theorem not_imp_not {a : Prop} {b : Prop} :
        ¬a¬b ba
        @[simp]
        theorem imp_and_neg_imp_iff (p : Prop) (q : Prop) :
        (pq) (¬pq) q
        theorem Function.mtr {a : Prop} {b : Prop} :
        (¬a¬b)ba

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

        theorem or_congr_left' {c : Prop} {a : Prop} {b : Prop} (h : ¬c(a b)) :
        a c b c
        theorem or_congr_right' {a : Prop} {b : Prop} {c : Prop} (h : ¬a(b c)) :
        a b a c

        Declarations about distributivity #

        Declarations about iff

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

        Alias of iff_congr.

        theorem iff_mpr_iff_true_intro {P : Prop} (h : P) :
        = h
        theorem imp_or {a : Prop} {b : Prop} {c : Prop} :
        ab c (ab) (ac)
        theorem imp_or' {a : Sort u_1} {b : Prop} {c : Prop} :
        ab c (ab) (ac)
        theorem not_imp {a : Prop} {b : Prop} :
        ¬(ab) a ¬b
        theorem peirce (a : Prop) (b : Prop) :
        ((ab)a)a
        theorem not_iff_not {a : Prop} {b : Prop} :
        (¬a ¬b) (a b)
        theorem not_iff_comm {a : Prop} {b : Prop} :
        (¬a b) (¬b a)
        theorem not_iff {a : Prop} {b : Prop} :
        ¬(a b) (¬a b)
        theorem iff_not_comm {a : Prop} {b : Prop} :
        (a ¬b) (b ¬a)
        theorem iff_iff_and_or_not_and_not {a : Prop} {b : Prop} :
        (a b) a b ¬a ¬b
        theorem iff_iff_not_or_and_or_not {a : Prop} {b : Prop} :
        (a b) (¬a b) (a ¬b)
        theorem not_and_not_right {a : Prop} {b : Prop} :
        ¬(a ¬b) ab

        De Morgan's laws #

        theorem not_and_or {a : Prop} {b : Prop} :
        ¬(a b) ¬a ¬b

        One of de Morgan's laws: the negation of a conjunction is logically equivalent to the disjunction of the negations.

        theorem or_iff_not_and_not {a : Prop} {b : Prop} :
        a b ¬(¬a ¬b)
        theorem and_iff_not_or_not {a : Prop} {b : Prop} :
        a b ¬(¬a ¬b)
        @[simp]
        theorem not_xor (P : Prop) (Q : Prop) :
        ¬Xor' P Q (P Q)
        theorem xor_iff_not_iff (P : Prop) (Q : Prop) :
        Xor' P Q ¬(P Q)
        theorem xor_iff_iff_not {a : Prop} {b : Prop} :
        Xor' a b (a ¬b)
        theorem xor_iff_not_iff' {a : Prop} {b : Prop} :
        Xor' a b (¬a b)

        Declarations about equality #

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

        Alias of ne_of_mem_of_not_mem.

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

        Alias of ne_of_mem_of_not_mem'.

        theorem ball_cond_comm {α : Sort u_1} {s : αProp} {p : ααProp} :
        (∀ (a : α), s a∀ (b : α), s bp a b) ∀ (a b : α), s as bp a b
        theorem ball_mem_comm {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {p : ααProp} :
        (∀ (a : α), a s∀ (b : α), b sp a b) ∀ (a b : α), a sb sp a b
        theorem ne_of_eq_of_ne :
        ∀ {α : Sort u_1} {a b c : α}, a = bb ca c
        theorem ne_of_ne_of_eq :
        ∀ {α : Sort u_1} {a b c : α}, a bb = ca c
        theorem Eq.trans_ne :
        ∀ {α : Sort u_1} {a b c : α}, a = bb ca c

        Alias of ne_of_eq_of_ne.

        theorem Ne.trans_eq :
        ∀ {α : Sort u_1} {a b c : α}, a bb = ca c

        Alias of ne_of_ne_of_eq.

        theorem eq_equivalence {α : Sort u_1} :
        theorem congr_refl_left {α : Sort u_1} {β : Sort u_2} (f : αβ) {a : α} {b : α} (h : a = b) :
        =
        theorem congr_refl_right {α : Sort u_1} {β : Sort u_2} {f : αβ} {g : αβ} (h : f = g) (a : α) :
        =
        theorem congr_arg_refl {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : α) :
        =
        theorem congr_fun_rfl {α : Sort u_1} {β : Sort u_2} (f : αβ) (a : α) :
        =
        theorem congr_fun_congr_arg {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) {a : α} {a' : α} (p : a = a') (b : β) :
        =
        theorem Eq.rec_eq_cast {α : Sort u_1} {P : αSort u_2} {x : α} {y : α} (h : x = y) (z : P x) :
        hz = cast z
        theorem eqRec_heq' {α : Sort u_1} {a' : α} {motive : (a : α) → a' = aSort u} (p : motive a' ) {a : α} (t : a' = a) :
        HEq (tp) p
        theorem rec_heq_of_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : αSort u_1} {x : C a} {y : β} (e : a = b) (h : HEq x y) :
        HEq (ex) y
        theorem rec_heq_iff_heq {α : Sort u_2} {a : α} {β : Sort u_1} {b : α} {C : αSort u_1} {x : C a} {y : β} {e : a = b} :
        HEq (ex) y HEq x y
        theorem heq_rec_iff_heq {α : Sort u_2} {β : Sort u_1} {a : α} {b : α} {C : αSort u_1} {x : β} {y : C a} {e : a = b} :
        HEq x (ey) HEq x y

        Declarations about quantifiers #

        theorem pi_congr {α : Sort u_5} {β : αSort u_1} {β' : αSort u_1} (h : ∀ (a : α), β a = β' a) :
        ((a : α) → β a) = ((a : α) → β' a)
        theorem forall₂_imp {α : Sort u_5} {β : αSort u_1} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a bq a b) :
        (∀ (a : α) (b : β a), p a b)∀ (a : α) (b : β a), q a b
        theorem forall₃_imp {α : Sort u_5} {β : αSort u_1} {γ : (a : α) → β aSort u_2} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b cq a b c) :
        (∀ (a : α) (b : β a) (c : γ a b), p a b c)∀ (a : α) (b : β a) (c : γ a b), q a b c
        theorem Exists₂.imp {α : Sort u_5} {β : αSort u_1} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a bq a b) :
        (∃ (a : α), ∃ (b : β a), p a b)∃ (a : α), ∃ (b : β a), q a b
        theorem Exists₃.imp {α : Sort u_5} {β : αSort u_1} {γ : (a : α) → β aSort u_2} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b cq a b c) :
        (∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), p a b c)∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), q a b c
        theorem forall_swap {α : Sort u_3} {β : Sort u_2} {p : αβProp} :
        (∀ (x : α) (y : β), p x y) ∀ (y : β) (x : α), p x y
        theorem forall₂_swap {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁Sort u_2} {κ₂ : ι₂Sort u_3} {p : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Prop} :
        (∀ (i₁ : ι₁) (j₁ : κ₁ i₁) (i₂ : ι₂) (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ∀ (i₂ : ι₂) (j₂ : κ₂ i₂) (i₁ : ι₁) (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
        theorem imp_forall_iff {α : Type u_2} {p : Prop} {q : αProp} :
        (p∀ (x : α), q x) ∀ (x : α), pq x

        We intentionally restrict the type of α in this lemma so that this is a safer to use in simp than forall_swap.

        theorem exists_swap {α : Sort u_3} {β : Sort u_2} {p : αβProp} :
        (∃ (x : α), ∃ (y : β), p x y) ∃ (y : β), ∃ (x : α), p x y
        theorem not_forall_not {α : Sort u_2} {p : αProp} :
        (¬∀ (x : α), ¬p x) ∃ (x : α), p x
        theorem forall_or_exists_not {α : Sort u_2} (P : αProp) :
        (∀ (a : α), P a) ∃ (a : α), ¬P a
        theorem exists_or_forall_not {α : Sort u_2} (P : αProp) :
        (∃ (a : α), P a) ∀ (a : α), ¬P a
        theorem forall_imp_iff_exists_imp {α : Sort u_2} {p : αProp} {b : Prop} [ha : Nonempty α] :
        (∀ (x : α), p x)b ∃ (x : α), p xb
        theorem forall_true_iff {α : Sort u_2} :
        αTrue True
        theorem forall_true_iff' {α : Sort u_2} {p : αProp} (h : ∀ (a : α), p a True) :
        (∀ (a : α), p a) True
        theorem forall₂_true_iff {α : Sort u_3} {β : αSort u_2} :
        (∀ (a : α), β aTrue) True
        theorem forall₃_true_iff {α : Sort u_4} {β : αSort u_2} {γ : (a : α) → β aSort u_3} :
        (∀ (a : α) (b : β a), γ a bTrue) True
        @[simp]
        theorem exists_unique_iff_exists {α : Sort u_2} [Subsingleton α] {p : αProp} :
        (∃! (x : α), p x) ∃ (x : α), p x
        theorem exists_unique_const {b : Prop} (α : Sort u_2) [i : Nonempty α] [Subsingleton α] :
        (∃! (x : α), b) b
        theorem Decidable.and_forall_ne {α : Sort u_2} [DecidableEq α] (a : α) {p : αProp} :
        (p a ∀ (b : α), b ap b) ∀ (b : α), p b
        theorem and_forall_ne {α : Sort u_2} {p : αProp} (a : α) :
        (p a ∀ (b : α), b ap b) ∀ (b : α), p b
        theorem Ne.ne_or_ne {α : Sort u_2} {x : α} {y : α} (z : α) (h : x y) :
        x z y z
        @[simp]
        theorem exists_unique_eq {α : Sort u_2} {a' : α} :
        ∃! (a : α), a = a'
        @[simp]
        theorem exists_unique_eq' {α : Sort u_2} {a' : α} :
        ∃! (a : α), a' = a
        theorem exists_apply_eq_apply' {α : Sort u_3} {β : Sort u_2} (f : αβ) (a' : α) :
        ∃ (a : α), f a' = f a
        theorem exists_apply_eq {α : Sort u_3} {β : Sort u_2} (a : α) (b : β) :
        ∃ (f : αβ), f a = b
        @[simp]
        theorem exists_exists_and_eq_and {α : Sort u_3} {β : Sort u_2} {f : αβ} {p : αProp} {q : βProp} :
        (∃ (b : β), (∃ (a : α), p a f a = b) q b) ∃ (a : α), p a q (f a)
        @[simp]
        theorem exists_exists_eq_and {α : Sort u_3} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∃ (b : β), (∃ (a : α), f a = b) p b) ∃ (a : α), p (f a)
        @[simp]
        theorem exists_exists_and_exists_and_eq_and {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {p : αProp} {q : βProp} {r : γProp} :
        (∃ (c : γ), (∃ (a : α), p a ∃ (b : β), q b f a b = c) r c) ∃ (a : α), p a ∃ (b : β), q b r (f a b)
        @[simp]
        theorem exists_exists_exists_and_eq {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {p : γProp} :
        (∃ (c : γ), (∃ (a : α), ∃ (b : β), f a b = c) p c) ∃ (a : α), ∃ (b : β), p (f a b)
        @[simp]
        theorem exists_or_eq_left {α : Sort u_2} (y : α) (p : αProp) :
        ∃ (x : α), x = y p x
        @[simp]
        theorem exists_or_eq_right {α : Sort u_2} (y : α) (p : αProp) :
        ∃ (x : α), p x x = y
        @[simp]
        theorem exists_or_eq_left' {α : Sort u_2} (y : α) (p : αProp) :
        ∃ (x : α), y = x p x
        @[simp]
        theorem exists_or_eq_right' {α : Sort u_2} (y : α) (p : αProp) :
        ∃ (x : α), p x y = x
        theorem forall_apply_eq_imp_iff' {α : Sort u_3} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∀ (a : α) (b : β), f a = bp b) ∀ (a : α), p (f a)
        theorem forall_eq_apply_imp_iff' {α : Sort u_3} {β : Sort u_2} {f : αβ} {p : βProp} :
        (∀ (a : α) (b : β), b = f ap b) ∀ (a : α), p (f a)
        @[simp]
        theorem exists_eq_right' {α : Sort u_2} {p : αProp} {a' : α} :
        (∃ (a : α), p a a' = a) p a'
        theorem exists₂_comm {ι₁ : Sort u_4} {ι₂ : Sort u_5} {κ₁ : ι₁Sort u_2} {κ₂ : ι₂Sort u_3} {p : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂Prop} :
        (∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), p i₁ j₁ i₂ j₂) ∃ (i₂ : ι₂), ∃ (j₂ : κ₂ i₂), ∃ (i₁ : ι₁), ∃ (j₁ : κ₁ i₁), p i₁ j₁ i₂ j₂
        theorem And.exists {p : Prop} {q : Prop} {f : p qProp} :
        (∃ (h : p q), f h) ∃ (hp : p), ∃ (hq : q), f
        theorem forall_or_of_or_forall {α : Sort u_2} {p : αProp} {b : Prop} (h : b ∀ (x : α), p x) (x : α) :
        b p x
        theorem Decidable.forall_or_left {α : Sort u_2} {q : Prop} {p : αProp} [Decidable q] :
        (∀ (x : α), q p x) q ∀ (x : α), p x
        theorem forall_or_left {α : Sort u_2} {q : Prop} {p : αProp} :
        (∀ (x : α), q p x) q ∀ (x : α), p x
        theorem Decidable.forall_or_right {α : Sort u_2} {q : Prop} {p : αProp} [Decidable q] :
        (∀ (x : α), p x q) (∀ (x : α), p x) q
        theorem forall_or_right {α : Sort u_2} {q : Prop} {p : αProp} :
        (∀ (x : α), p x q) (∀ (x : α), p x) q
        theorem exists_unique_prop {p : Prop} {q : Prop} :
        (∃! (x : p), q) p q
        @[simp]
        theorem exists_unique_false {α : Sort u_2} :
        ¬∃! (x : α), False
        theorem Exists.fst {b : Prop} {p : bProp} :
        Exists pb
        theorem Exists.snd {b : Prop} {p : bProp} (h : Exists p) :
        p
        theorem Prop.exists_iff {p : PropProp} :
        (∃ (h : Prop), p h) p False p True
        theorem Prop.forall_iff {p : PropProp} :
        (∀ (h : Prop), p h) p False p True
        theorem exists_prop_of_true {p : Prop} {q : pProp} (h : p) :
        (∃ (h' : p), q h') q h
        theorem exists_iff_of_forall {p : Prop} {q : pProp} (h : ∀ (h : p), q h) :
        (∃ (h : p), q h) p
        theorem exists_unique_prop_of_true {p : Prop} {q : pProp} (h : p) :
        (∃! (h' : p), q h') q h
        theorem exists_prop_of_false {p : Prop} {q : pProp} :
        ¬p¬∃ (h' : p), q h'
        theorem exists_prop_congr {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        Exists q ∃ (h : p'), q'
        theorem exists_prop_congr' {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        Exists q = ∃ (h : p'), q'
        @[simp]
        theorem exists_true_left (p : TrueProp) :
        (∃ (x : True), p x) p True.intro

        See IsEmpty.exists_iff for the False version.

        theorem forall_prop_congr {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        (∀ (h : p), q h) ∀ (h : p'), q'
        theorem forall_prop_congr' {p : Prop} {p' : Prop} {q : pProp} {q' : pProp} (hq : ∀ (h : p), q h q' h) (hp : p p') :
        (∀ (h : p), q h) = ∀ (h : p'), q'
        @[simp]
        theorem forall_true_left (p : TrueProp) :
        (∀ (x : True), p x) p True.intro

        See IsEmpty.forall_iff for the False version.

        theorem ExistsUnique.elim₂ {α : Sort u_2} {p : αSort u_3} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} {b : Prop} (h₂ : ∃! (x : α), ∃! (h : p x), q x h) (h₁ : ∀ (x : α) (h : p x), q x h(∀ (y : α) (hy : p y), q y hyy = x)b) :
        b
        theorem ExistsUnique.intro₂ {α : Sort u_2} {p : αSort u_3} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} (w : α) (hp : p w) (hq : q w hp) (H : ∀ (y : α) (hy : p y), q y hyy = w) :
        ∃! (x : α), ∃! (hx : p x), q x hx
        theorem ExistsUnique.exists₂ {α : Sort u_2} {p : αSort u_3} {q : (x : α) → p xProp} (h : ∃! (x : α), ∃! (hx : p x), q x hx) :
        ∃ (x : α), ∃ (hx : p x), q x hx
        theorem ExistsUnique.unique₂ {α : Sort u_2} {p : αSort u_3} [∀ (x : α), Subsingleton (p x)] {q : (x : α) → p xProp} (h : ∃! (x : α), ∃! (hx : p x), q x hx) {y₁ : α} {y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) :
        y₁ = y₂

        Classical lemmas #

        noncomputable def Classical.dec (p : Prop) :

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

        Equations
        Instances For
          noncomputable def Classical.decPred {α : Sort u_1} (p : αProp) :

          Any predicate p is decidable classically.

          Equations
          Instances For
            noncomputable def Classical.decRel {α : Sort u_1} (p : ααProp) :

            Any relation p is decidable classically.

            Equations
            Instances For
              noncomputable def Classical.decEq (α : Sort u) :

              Any type α has decidable equality classically.

              Equations
              Instances For
                noncomputable def Classical.existsCases {α : Prop} {p : αProp} {C : Sort u_1} (H0 : C) (H : (a : α) → p aC) :
                C

                Construct a function from a default value H0, and a function to use if there exists a value satisfying the predicate.

                Equations
                Instances For
                  theorem Classical.some_spec₂ {α : Sort u_1} {p : αProp} {h : ∃ (a : α), p a} (q : αProp) (hpq : ∀ (a : α), p aq a) :
                  noncomputable def Classical.subtype_of_exists {α : Type u_1} {P : αProp} (h : ∃ (x : α), P x) :
                  { x : α // P x }

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

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

                    A version of byContradiction that uses types instead of propositions.

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

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

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

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

                        Equations
                        Instances For

                          Declarations about bounded quantifiers #

                          theorem bex_def {α : Sort u_1} {p : αProp} {q : αProp} :
                          (∃ (x : α), ∃ (x_1 : p x), q x) ∃ (x : α), p x q x
                          theorem BEx.elim {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {b : Prop} :
                          (∃ (x : α), ∃ (h : p x), P x h)(∀ (a : α) (h : p a), P a hb)b
                          theorem BEx.intro {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} (a : α) (h₁ : p a) (h₂ : P a h₁) :
                          ∃ (x : α), ∃ (h : p x), P x h
                          theorem ball_congr {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x h Q x h) :
                          (∀ (x : α) (h : p x), P x h) ∀ (x : α) (h : p x), Q x h
                          theorem bex_congr {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x h Q x h) :
                          (∃ (x : α), ∃ (h : p x), P x h) ∃ (x : α), ∃ (h : p x), Q x h
                          theorem bex_eq_left {α : Sort u_1} {p : αProp} {a : α} :
                          (∃ (x : α), ∃ (x_1 : x = a), p x) p a
                          theorem BAll.imp_right {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x hQ x h) (h₁ : ∀ (x : α) (h : p x), P x h) (x : α) (h : p x) :
                          Q x h
                          theorem BEx.imp_right {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} (H : ∀ (x : α) (h : p x), P x hQ x h) :
                          (∃ (x : α), ∃ (h : p x), P x h)∃ (x : α), ∃ (h : p x), Q x h
                          theorem BAll.imp_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} (H : ∀ (x : α), p xq x) (h₁ : ∀ (x : α), q xr x) (x : α) (h : p x) :
                          r x
                          theorem BEx.imp_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} (H : ∀ (x : α), p xq x) :
                          (∃ (x : α), ∃ (x_1 : p x), r x)∃ (x : α), ∃ (x_1 : q x), r x
                          theorem ball_of_forall {α : Sort u_1} {p : αProp} (h : ∀ (x : α), p x) (x : α) :
                          p x
                          theorem forall_of_ball {α : Sort u_1} {p : αProp} {q : αProp} (H : ∀ (x : α), p x) (h : ∀ (x : α), p xq x) (x : α) :
                          q x
                          theorem bex_of_exists {α : Sort u_1} {p : αProp} {q : αProp} (H : ∀ (x : α), p x) :
                          (∃ (x : α), q x)∃ (x : α), ∃ (x_1 : p x), q x
                          theorem exists_of_bex {α : Sort u_1} {p : αProp} {q : αProp} :
                          (∃ (x : α), ∃ (x_1 : p x), q x)∃ (x : α), q x
                          theorem bex_imp {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {b : Prop} :
                          (∃ (x : α), ∃ (h : p x), P x h)b ∀ (x : α) (h : p x), P x hb
                          theorem not_bex {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                          (¬∃ (x : α), ∃ (h : p x), P x h) ∀ (x : α) (h : p x), ¬P x h
                          theorem not_ball_of_bex_not {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                          (∃ (x : α), ∃ (h : p x), ¬P x h)¬∀ (x : α) (h : p x), P x h
                          theorem Decidable.not_ball {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} [Decidable (∃ (x : α), ∃ (h : p x), ¬P x h)] [(x : α) → (h : p x) → Decidable (P x h)] :
                          (¬∀ (x : α) (h : p x), P x h) ∃ (x : α), ∃ (h : p x), ¬P x h
                          theorem not_ball {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} :
                          (¬∀ (x : α) (h : p x), P x h) ∃ (x : α), ∃ (h : p x), ¬P x h
                          theorem ball_true_iff {α : Sort u_1} (p : αProp) :
                          (∀ (x : α), p xTrue) True
                          theorem ball_and {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} :
                          (∀ (x : α) (h : p x), P x h Q x h) (∀ (x : α) (h : p x), P x h) ∀ (x : α) (h : p x), Q x h
                          theorem bex_or {α : Sort u_1} {p : αProp} {P : (x : α) → p xProp} {Q : (x : α) → p xProp} :
                          (∃ (x : α), ∃ (h : p x), P x h Q x h) (∃ (x : α), ∃ (h : p x), P x h) ∃ (x : α), ∃ (h : p x), Q x h
                          theorem ball_or_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} :
                          (∀ (x : α), p x q xr x) (∀ (x : α), p xr x) ∀ (x : α), q xr x
                          theorem bex_or_left {α : Sort u_1} {r : αProp} {p : αProp} {q : αProp} :
                          (∃ (x : α), ∃ (x_1 : p x q x), r x) (∃ (x : α), ∃ (x_1 : p x), r x) ∃ (x : α), ∃ (x_1 : q x), r x
                          theorem dite_eq_iff {α : Sort u_2} {P : Prop} [Decidable P] {c : α} {A : Pα} {B : ¬Pα} :
                          dite P A B = c (∃ (h : P), A h = c) ∃ (h : ¬P), B h = c
                          theorem ite_eq_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                          (if P then a else b) = c P a = c ¬P b = c
                          theorem eq_ite_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                          (a = if P then b else c) P a = b ¬P a = c
                          theorem dite_eq_iff' {α : Sort u_2} {P : Prop} [Decidable P] {c : α} {A : Pα} {B : ¬Pα} :
                          dite P A B = c (∀ (h : P), A h = c) ∀ (h : ¬P), B h = c
                          theorem ite_eq_iff' {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} {c : α} :
                          (if P then a else b) = c (Pa = c) (¬Pb = c)
                          theorem dite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} :
                          dite P (fun (x : P) => a) B a ∃ (h : ¬P), a B h
                          theorem dite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : Pα} :
                          (dite P A fun (x : ¬P) => b) b ∃ (h : P), A h b
                          theorem ite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} :
                          (if P then a else b) a ¬P a b
                          theorem ite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} :
                          (if P then a else b) b P a b
                          theorem Ne.dite_eq_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} (h : ∀ (h : ¬P), a B h) :
                          dite P (fun (x : P) => a) B = a P
                          theorem Ne.dite_eq_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : Pα} (h : ∀ (h : P), A h b) :
                          (dite P A fun (x : ¬P) => b) = b ¬P
                          theorem Ne.ite_eq_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                          (if P then a else b) = a P
                          theorem Ne.ite_eq_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                          (if P then a else b) = b ¬P
                          theorem Ne.dite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {B : ¬Pα} (h : ∀ (h : ¬P), a B h) :
                          dite P (fun (x : P) => a) B a ¬P
                          theorem Ne.dite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {b : α} {A : Pα} (h : ∀ (h : P), A h b) :
                          (dite P A fun (x : ¬P) => b) b P
                          theorem Ne.ite_ne_left_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                          (if P then a else b) a ¬P
                          theorem Ne.ite_ne_right_iff {α : Sort u_2} {P : Prop} [Decidable P] {a : α} {b : α} (h : a b) :
                          (if P then a else b) b P
                          theorem dite_eq_or_eq {α : Sort u_2} (P : Prop) [Decidable P] {A : Pα} {B : ¬Pα} :
                          (∃ (h : P), dite P A B = A h) ∃ (h : ¬P), dite P A B = B h
                          theorem ite_eq_or_eq {α : Sort u_2} (P : Prop) [Decidable P] (a : α) (b : α) :
                          (if P then a else b) = a (if P then a else b) = b
                          theorem apply_dite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_2} (f : αβγ) (P : Prop) [Decidable P] (a : Pα) (b : ¬Pα) (c : Pβ) (d : ¬Pβ) :
                          f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

                          A two-argument function applied to two dites is a dite of that two-argument function applied to each of the branches.

                          theorem apply_ite₂ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_2} (f : αβγ) (P : Prop) [Decidable P] (a : α) (b : α) (c : β) (d : β) :
                          f (if P then a else b) (if P then c else d) = if P then f a c else f b d

                          A two-argument function applied to two ites is a ite of that two-argument function applied to each of the branches.

                          theorem dite_apply {α : Sort u_2} {σ : αSort u_1} (P : Prop) [Decidable P] (f : P(a : α) → σ a) (g : ¬P(a : α) → σ a) (a : α) :
                          dite P f g a = if h : P then f h a else g h a

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

                          theorem ite_apply {α : Sort u_2} {σ : αSort u_1} (P : Prop) [Decidable P] (f : (a : α) → σ a) (g : (a : α) → σ a) (a : α) :
                          (if P then f else g) a = if P then f a else g a

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

                          theorem ite_and {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) :
                          (if P Q then a else b) = if P then if Q then a else b else b
                          theorem dite_dite_comm {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] {A : Pα} {B : Qα} {C : ¬P¬Qα} (h : P¬Q) :
                          (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q
                          theorem ite_ite_comm {α : Sort u_2} (P : Prop) (Q : Prop) [Decidable P] [Decidable Q] (a : α) (b : α) {c : α} (h : P¬Q) :
                          (if P then a else if Q then b else c) = if Q then b else if P then a else c
                          theorem ite_prop_iff_or {P : Prop} {Q : Prop} {R : Prop} [Decidable P] :
                          (if P then Q else R) P Q ¬P R
                          theorem dite_prop_iff_or {P : Prop} {Q : PProp} {R : ¬PProp} [Decidable P] :
                          dite P Q R (∃ (p : P), Q p) ∃ (p : ¬P), R p
                          theorem ite_prop_iff_and {P : Prop} {Q : Prop} {R : Prop} [Decidable P] :
                          (if P then Q else R) (PQ) (¬PR)
                          theorem dite_prop_iff_and {P : Prop} {Q : PProp} {R : ¬PProp} [Decidable P] :
                          dite P Q R (∀ (h : P), Q h) ∀ (h : ¬P), R h
                          @[simp]
                          theorem if_true_right {P : Prop} {Q : Prop} [Decidable P] :
                          (if P then Q else True) ¬P Q
                          @[simp]
                          theorem if_true_left {P : Prop} {Q : Prop} [Decidable P] :
                          (if P then True else Q) P Q
                          @[simp]
                          theorem if_false_right {P : Prop} {Q : Prop} [Decidable P] :
                          (if P then Q else False) P Q
                          @[simp]
                          theorem if_false_left {P : Prop} {Q : Prop} [Decidable P] :
                          (if P then False else Q) ¬P Q
                          theorem not_beq_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} (ne : a b) :
                          ¬(a == b) = true
                          theorem beq_eq_decide {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {b : α} :
                          (a == b) = decide (a = b)
                          theorem beq_ext {α : Type u_1} (inst1 : BEq α) (inst2 : BEq α) (h : ∀ (x y : α), (x == y) = (x == y)) :
                          inst1 = inst2
                          theorem lawful_beq_subsingleton {α : Type u_1} (inst1 : BEq α) (inst2 : BEq α) [LawfulBEq α] [LawfulBEq α] :
                          inst1 = inst2