Documentation

Std.Logic

instance instDecidablePredCompProp {α : Sort u_1} {β : Sort u_2} {p : βProp} {f : αβ} [DecidablePred p] :

not #

theorem Not.intro {a : Prop} (h : aFalse) :
def Not.elim {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) :
α

Ex falso for negation. From ¬a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the not namespace so that projection notation can be used.

Instances For
    theorem Not.imp {a : Prop} {b : Prop} (H2 : ¬b) (H1 : ab) :
    theorem not_congr {a : Prop} {b : Prop} (h : a b) :
    theorem not_not_of_not_imp {a : Prop} {b : Prop} :
    ¬(ab)¬¬a
    theorem not_of_not_imp {b : Prop} {a : Prop} :
    ¬(ab)¬b
    @[simp]
    theorem imp_not_self {a : Prop} :
    a¬a ¬a

    iff #

    theorem iff_def {a : Prop} {b : Prop} :
    (a b) (ab) (ba)
    theorem iff_def' {a : Prop} {b : Prop} :
    (a b) (ba) (ab)
    def Iff.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : (ab) → (ba) → α) (h : a b) :
    α

    Non-dependent eliminator for Iff.

    Instances For
      theorem Eq.to_iff {a : Prop} {b : Prop} :
      a = b → (a b)
      theorem iff_of_eq {a : Prop} {b : Prop} :
      a = b → (a b)
      theorem neq_of_not_iff {a : Prop} {b : Prop} :
      ¬(a b)a b
      theorem iff_iff_eq {a : Prop} {b : Prop} :
      (a b) a = b
      @[simp]
      theorem eq_iff_iff {p : Prop} {q : Prop} :
      p = q (p q)
      theorem of_iff_true {a : Prop} (h : a True) :
      a
      theorem not_of_iff_false {a : Prop} :
      (a False) → ¬a
      theorem iff_of_true {a : Prop} {b : Prop} (ha : a) (hb : b) :
      a b
      theorem iff_of_false {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
      a b
      theorem iff_true_left {a : Prop} {b : Prop} (ha : a) :
      (a b) b
      theorem iff_true_right {a : Prop} {b : Prop} (ha : a) :
      (b a) b
      theorem iff_false_left {a : Prop} {b : Prop} (ha : ¬a) :
      (a b) ¬b
      theorem iff_false_right {a : Prop} {b : Prop} (ha : ¬a) :
      (b a) ¬b
      theorem iff_true_intro {a : Prop} (h : a) :
      theorem iff_false_intro {a : Prop} (h : ¬a) :
      theorem not_iff_false_intro {a : Prop} (h : a) :
      theorem iff_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
      (a b) (c d)
      @[simp]
      theorem ne_self_iff_false {α : Sort u_1} (a : α) :
      theorem eq_self_iff_true {α : Sort u_1} (a : α) :
      a = a True
      theorem heq_self_iff_true {α : Sort u_1} (a : α) :
      theorem iff_not_self {a : Prop} :
      ¬(a ¬a)
      @[simp]
      theorem not_iff_self {a : Prop} :
      ¬(¬a a)
      theorem eq_comm {α : Sort u_1} {a : α} {b : α} :
      a = b b = a

      implies #

      theorem imp_intro {α : Prop} {β : Prop} (h : α) :
      βα
      theorem imp_imp_imp {a : Prop} {b : Prop} {c : Prop} {d : Prop} (h₀ : ca) (h₁ : bd) :
      (ab) → cd
      theorem imp_iff_right {b : Prop} {a : Prop} (ha : a) :
      ab b
      theorem imp_true_iff (α : Sort u) :
      αTrue True
      theorem false_imp_iff (a : Prop) :
      Falsea True
      theorem true_imp_iff (α : Prop) :
      Trueα α
      @[simp]
      theorem imp_self {a : Prop} :
      aa True
      theorem imp_false {a : Prop} :
      aFalse ¬a
      theorem imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} :
      abc bac
      theorem imp_not_comm {a : Prop} {b : Prop} :
      a¬b b¬a
      theorem imp_congr_left {a : Prop} {b : Prop} {c : Prop} (h : a b) :
      ac bc
      theorem imp_congr_right {a : Sort u_1} {b : Prop} {c : Prop} (h : a → (b c)) :
      ab ac
      theorem imp_congr_ctx {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : c → (b d)) :
      ab cd
      theorem imp_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
      ab cd
      theorem imp_iff_not {b : Prop} {a : Prop} (hb : ¬b) :
      ab ¬a

      and #

      @[inline, reducible]
      abbrev And.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : abα) (h : a b) :
      α

      Non-dependent eliminator for And.

      Instances For
        theorem And.symm {a : Prop} {b : Prop} :
        a bb a
        theorem And.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : ac) (g : bd) (h : a b) :
        c d
        theorem And.imp_left {a : Prop} {b : Prop} {c : Prop} (h : ab) :
        a cb c
        theorem And.imp_right {a : Prop} {b : Prop} {c : Prop} (h : ab) :
        c ac b
        theorem and_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
        a b c d
        theorem and_comm {a : Prop} {b : Prop} :
        a b b a
        theorem and_congr_right {a : Prop} {b : Prop} {c : Prop} (h : a → (b c)) :
        a b a c
        theorem and_congr_left {c : Prop} {a : Prop} {b : Prop} (h : c → (a b)) :
        a c b c
        theorem and_congr_left' {a : Prop} {b : Prop} {c : Prop} (h : a b) :
        a c b c
        theorem and_congr_right' {b : Prop} {c : Prop} {a : Prop} (h : b c) :
        a b a c
        theorem and_congr_right_eq {a : Prop} {b : Prop} {c : Prop} (h : ab = c) :
        (a b) = (a c)
        theorem and_congr_left_eq {c : Prop} {a : Prop} {b : Prop} (h : ca = b) :
        (a c) = (b c)
        theorem and_assoc {a : Prop} {b : Prop} {c : Prop} :
        (a b) c a b c
        theorem and_left_comm {a : Prop} {b : Prop} {c : Prop} :
        a b c b a c
        theorem and_right_comm {a : Prop} {b : Prop} {c : Prop} :
        (a b) c (a c) b
        theorem and_rotate {a : Prop} {b : Prop} {c : Prop} :
        a b c b c a
        theorem and_and_and_comm {a : Prop} {b : Prop} {c : Prop} {d : Prop} :
        (a b) c d (a c) b d
        theorem and_and_left {a : Prop} {b : Prop} {c : Prop} :
        a b c (a b) a c
        theorem and_and_right {a : Prop} {b : Prop} {c : Prop} :
        (a b) c (a c) b c
        theorem and_iff_left_of_imp {a : Prop} {b : Prop} (h : ab) :
        a b a
        theorem and_iff_right_of_imp {b : Prop} {a : Prop} (h : ba) :
        a b b
        theorem and_iff_left {b : Prop} {a : Prop} (hb : b) :
        a b a
        theorem and_iff_right {a : Prop} {b : Prop} (ha : a) :
        a b b
        @[simp]
        theorem and_iff_left_iff_imp {a : Prop} {b : Prop} :
        (a b a) ab
        @[simp]
        theorem and_iff_right_iff_imp {a : Prop} {b : Prop} :
        (a b b) ba
        @[simp]
        theorem iff_self_and {p : Prop} {q : Prop} :
        (p p q) pq
        @[simp]
        theorem iff_and_self {p : Prop} {q : Prop} :
        (p q p) pq
        @[simp]
        theorem and_congr_right_iff {a : Prop} {b : Prop} {c : Prop} :
        (a b a c) a → (b c)
        @[simp]
        theorem and_congr_left_iff {a : Prop} {c : Prop} {b : Prop} :
        (a c b c) c → (a b)
        @[simp]
        theorem and_self_left {a : Prop} {b : Prop} :
        a a b a b
        @[simp]
        theorem and_self_right {a : Prop} {b : Prop} :
        (a b) b a b
        theorem not_and_of_not_left {a : Prop} (b : Prop) :
        ¬a¬(a b)
        theorem not_and_of_not_right (a : Prop) {b : Prop} :
        ¬b¬(a b)
        @[simp]
        theorem and_not_self {a : Prop} :
        ¬(a ¬a)
        @[simp]
        theorem not_and_self {a : Prop} :
        ¬(¬a a)

        or #

        theorem not_not_em (a : Prop) :
        ¬¬(a ¬a)
        theorem Or.symm {a : Prop} {b : Prop} :
        a bb a
        theorem Or.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : ac) (g : bd) (h : a b) :
        c d
        theorem Or.imp_left {a : Prop} {b : Prop} {c : Prop} (f : ab) :
        a cb c
        theorem Or.imp_right {b : Prop} {c : Prop} {a : Prop} (f : bc) :
        a ba c
        theorem or_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a c) (h₂ : b d) :
        a b c d
        theorem or_congr_left {a : Prop} {b : Prop} {c : Prop} (h : a b) :
        a c b c
        theorem or_congr_right {b : Prop} {c : Prop} {a : Prop} (h : b c) :
        a b a c
        theorem Or.comm {a : Prop} {b : Prop} :
        a b b a
        theorem or_comm {a : Prop} {b : Prop} :
        a b b a
        theorem or_assoc {a : Prop} {b : Prop} {c : Prop} :
        (a b) c a b c
        theorem Or.resolve_left {a : Prop} {b : Prop} (h : a b) (na : ¬a) :
        b
        theorem Or.neg_resolve_left {a : Prop} {b : Prop} (h : ¬a b) (ha : a) :
        b
        theorem Or.resolve_right {a : Prop} {b : Prop} (h : a b) (nb : ¬b) :
        a
        theorem Or.neg_resolve_right {a : Prop} {b : Prop} (h : a ¬b) (nb : b) :
        a
        theorem or_left_comm {a : Prop} {b : Prop} {c : Prop} :
        a b c b a c
        theorem or_right_comm {a : Prop} {b : Prop} {c : Prop} :
        (a b) c (a c) b
        theorem or_or_or_comm {a : Prop} {b : Prop} {c : Prop} {d : Prop} :
        (a b) c d (a c) b d
        theorem or_or_distrib_left {a : Prop} {b : Prop} {c : Prop} :
        a b c (a b) a c
        theorem or_or_distrib_right {a : Prop} {b : Prop} {c : Prop} :
        (a b) c (a c) b c
        theorem or_rotate {a : Prop} {b : Prop} {c : Prop} :
        a b c b c a
        theorem or_iff_right_of_imp {a : Prop} {b : Prop} (ha : ab) :
        a b b
        theorem or_iff_left_of_imp {b : Prop} {a : Prop} (hb : ba) :
        a b a
        theorem not_or_intro {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
        ¬(a b)
        @[simp]
        theorem or_iff_left_iff_imp {a : Prop} {b : Prop} :
        (a b a) ba
        @[simp]
        theorem or_iff_right_iff_imp {a : Prop} {b : Prop} :
        (a b b) ab
        theorem or_iff_left {b : Prop} {a : Prop} (hb : ¬b) :
        a b a
        theorem or_iff_right {a : Prop} {b : Prop} (ha : ¬a) :
        a b b

        distributivity #

        theorem not_imp_of_and_not {a : Prop} {b : Prop} :
        a ¬b¬(ab)
        theorem imp_and {b : Prop} {c : Prop} {α : Sort u_1} :
        αb c (αb) (αc)
        @[simp]
        theorem and_imp {a : Prop} {b : Prop} {c : Prop} :
        a bc abc
        @[simp]
        theorem not_and {a : Prop} {b : Prop} :
        ¬(a b) a¬b
        theorem not_and' {a : Prop} {b : Prop} :
        ¬(a b) b¬a
        theorem and_or_left {a : Prop} {b : Prop} {c : Prop} :
        a (b c) a b a c

        distributes over (on the left).

        theorem or_and_right {a : Prop} {b : Prop} {c : Prop} :
        (a b) c a c b c

        distributes over (on the right).

        theorem or_and_left {a : Prop} {b : Prop} {c : Prop} :
        a b c (a b) (a c)

        distributes over (on the left).

        theorem and_or_right {a : Prop} {b : Prop} {c : Prop} :
        a b c (a c) (b c)

        distributes over (on the right).

        theorem or_imp {a : Prop} {b : Prop} {c : Prop} :
        a bc (ac) (bc)
        theorem not_or {p : Prop} {q : Prop} :
        ¬(p q) ¬p ¬q
        theorem not_and_of_not_or_not {a : Prop} {b : Prop} (h : ¬a ¬b) :
        ¬(a b)
        @[simp]
        theorem or_self_left {a : Prop} {b : Prop} :
        a a b a b
        @[simp]
        theorem or_self_right {a : Prop} {b : Prop} :
        (a b) b a b

        exists and forall #

        theorem forall_imp {α : Sort u_1} {p : αProp} {q : αProp} (h : (a : α) → p aq a) :
        ((a : α) → p a) → (a : α) → q a
        @[simp]
        theorem forall_exists_index {α : Sort u_1} {p : αProp} {q : (x, p x) → Prop} :
        ((h : x, p x) → q h) (x : α) → (h : p x) → q (_ : x, p x)
        theorem Exists.imp {α : Sort u_1} {p : αProp} {q : αProp} (h : (a : α) → p aq a) :
        (a, p a) → a, q a
        theorem Exists.imp' {α : Sort u_2} {p : αProp} {β : Sort u_1} {q : βProp} (f : αβ) (hpq : (a : α) → p aq (f a)) :
        (a, p a) → b, q b
        theorem exists_imp {α : Sort u_1} {p : αProp} {b : Prop} :
        (x, p x) → b (x : α) → p xb
        theorem forall_congr' {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (a : α), p a q a) :
        ((a : α) → p a) (a : α) → q a
        theorem exists_congr {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (a : α), p a q a) :
        (a, p a) a, q a
        theorem forall₂_congr {α : Sort u_1} {β : αSort u_2} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a b q a b) :
        ((a : α) → (b : β a) → p a b) (a : α) → (b : β a) → q a b
        theorem exists₂_congr {α : Sort u_1} {β : αSort u_2} {p : (a : α) → β aProp} {q : (a : α) → β aProp} (h : ∀ (a : α) (b : β a), p a b q a b) :
        (a b, p a b) a b, q a b
        theorem forall₃_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
        ((a : α) → (b : β a) → (c : γ a b) → p a b c) (a : α) → (b : β a) → (c : γ a b) → q a b c
        theorem exists₃_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {p : (a : α) → (b : β a) → γ a bProp} {q : (a : α) → (b : β a) → γ a bProp} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c q a b c) :
        (a b c, p a b c) a b c, q a b c
        theorem forall₄_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), p a b c d q a b c d) :
        ((a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → p a b c d) (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → q a b c d
        theorem exists₄_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b cProp} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c), 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
        theorem forall₅_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b cSort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), p a b c d e q a b c d e) :
        ((a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → (e : ε a b c d) → p a b c d e) (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → (e : ε a b c d) → q a b c d e
        theorem exists₅_congr {α : Sort u_1} {β : αSort u_2} {γ : (a : α) → β aSort u_3} {δ : (a : α) → (b : β a) → γ a bSort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b cSort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c dProp} (h : ∀ (a : α) (b : β a) (c : γ a b) (d : δ a b c) (e : ε a b c d), 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
        @[simp]
        theorem not_exists {α : Sort u_1} {p : αProp} :
        (¬x, p x) ∀ (x : α), ¬p x
        theorem forall_not_of_not_exists {α : Sort u_1} {p : αProp} (hne : ¬x, p x) (x : α) :
        ¬p x
        theorem forall_and {α : Sort u_1} {p : αProp} {q : αProp} :
        (∀ (x : α), p x q x) ((x : α) → p x) ((x : α) → q x)
        theorem exists_or {α : Sort u_1} {p : αProp} {q : αProp} :
        (x, p x q x) (x, p x) x, q x
        @[simp]
        theorem exists_false {α : Sort u_1} :
        ¬_a, False
        @[simp]
        theorem forall_const {b : Prop} (α : Sort u_1) [i : Nonempty α] :
        αb b
        theorem Exists.nonempty {α : Sort u_1} {p : αProp} :
        (x, p x) → Nonempty α
        @[reducible]
        noncomputable def Exists.choose {α : Sort u_1} {p : αProp} (P : a, p a) :
        α

        Extract an element from a existential statement, using Classical.choose.

        Instances For
          theorem Exists.choose_spec {α : Sort u_1} {p : αProp} (P : a, p a) :

          Show that an element extracted from P : ∃ a, p a using P.choose satisfies p.

          theorem not_forall_of_exists_not {α : Sort u_1} {p : αProp} :
          (x, ¬p x) → ¬((x : α) → p x)
          @[simp]
          theorem forall_eq {α : Sort u_1} {p : αProp} {a' : α} :
          ((a : α) → a = a'p a) p a'
          @[simp]
          theorem forall_eq' {α : Sort u_1} {p : αProp} {a' : α} :
          ((a : α) → a' = ap a) p a'
          @[simp]
          theorem exists_eq :
          ∀ {α : Sort u_1} {a' : α}, a, a = a'
          @[simp]
          theorem exists_eq' :
          ∀ {α : Sort u_1} {a' : α}, a, a' = a
          @[simp]
          theorem exists_eq_left {α : Sort u_1} {p : αProp} {a' : α} :
          (a, a = a' p a) p a'
          @[simp]
          theorem exists_eq_right {α : Sort u_1} {p : αProp} {a' : α} :
          (a, p a a = a') p a'
          @[simp]
          theorem exists_and_left {α : Sort u_1} {p : αProp} {b : Prop} :
          (x, b p x) b x, p x
          @[simp]
          theorem exists_and_right {α : Sort u_1} {p : αProp} {b : Prop} :
          (x, p x b) (x, p x) b
          @[simp]
          theorem exists_eq_left' {α : Sort u_1} {p : αProp} {a' : α} :
          (a, a' = a p a) p a'
          @[simp]
          theorem forall_eq_or_imp {α : Sort u_1} {p : αProp} {q : αProp} {a' : α} :
          ((a : α) → a = a' q ap a) p a' ((a : α) → q ap a)
          @[simp]
          theorem exists_eq_or_imp {α : Sort u_1} {p : αProp} {q : αProp} {a' : α} :
          (a, (a = a' q a) p a) p a' a, q a p a
          @[simp]
          theorem exists_eq_right_right {α : Sort u_1} {p : αProp} {b : Prop} {a' : α} :
          (a, p a b a = a') p a' b
          @[simp]
          theorem exists_eq_right_right' {α : Sort u_1} {p : αProp} {b : Prop} {a' : α} :
          (a, p a b a' = a) p a' b
          @[simp]
          theorem exists_prop {b : Prop} {a : Prop} :
          (_h, b) a b
          @[simp]
          theorem exists_apply_eq_apply {α : Sort u_2} {β : Sort u_1} (f : αβ) (a' : α) :
          a, f a = f a'
          theorem forall_prop_of_true {p : Prop} {q : pProp} (h : p) :
          ((h' : p) → q h') q h
          theorem forall_comm {α : Sort u_2} {β : Sort u_1} {p : αβProp} :
          ((a : α) → (b : β) → p a b) (b : β) → (a : α) → p a b
          theorem exists_comm {α : Sort u_2} {β : Sort u_1} {p : αβProp} :
          (a b, p a b) b a, p a b

          decidable #

          theorem Decidable.by_contra {p : Prop} [Decidable p] :
          (¬pFalse) → p
          def Or.by_cases {p : Prop} {q : Prop} [Decidable p] {α : Sort u} (h : p q) (h₁ : pα) (h₂ : qα) :
          α

          Construct a non-Prop by cases on an Or, when the left conjunct is decidable.

          Instances For
            def Or.by_cases' {q : Prop} {p : Prop} [Decidable q] {α : Sort u} (h : p q) (h₁ : pα) (h₂ : qα) :
            α

            Construct a non-Prop by cases on an Or, when the right conjunct is decidable.

            Instances For
              instance exists_prop_decidable {p : Prop} (P : pProp) [Decidable p] [(h : p) → Decidable (P h)] :
              Decidable (h, P h)
              instance forall_prop_decidable {p : Prop} (P : pProp) [Decidable p] [(h : p) → Decidable (P h)] :
              Decidable ((h : p) → P h)
              @[simp]
              theorem decide_eq_decide {p : Prop} {q : Prop} [Decidable p] [Decidable q] :
              decide p = decide q (p q)
              theorem Decidable.of_not_imp {a : Prop} {b : Prop} [Decidable a] (h : ¬(ab)) :
              a
              theorem Decidable.not_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬ab) (hb : ¬b) :
              a
              theorem Decidable.not_imp_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] :
              ¬ab ¬ba
              theorem Decidable.not_imp_self {a : Prop} [Decidable a] :
              ¬aa a
              theorem Decidable.or_iff_not_imp_left {a : Prop} {b : Prop} [Decidable a] :
              a b ¬ab
              theorem Decidable.or_iff_not_imp_right {b : Prop} {a : Prop} [Decidable b] :
              a b ¬ba
              theorem Decidable.not_imp_not {a : Prop} {b : Prop} [Decidable a] :
              ¬a¬b ba
              theorem Decidable.not_or_of_imp {a : Prop} {b : Prop} [Decidable a] (h : ab) :
              ¬a b
              theorem Decidable.imp_iff_not_or {a : Prop} {b : Prop} [Decidable a] :
              ab ¬a b
              theorem Decidable.imp_iff_or_not {b : Prop} {a : Prop} [Decidable b] :
              ba a ¬b
              theorem Decidable.imp_or {a : Prop} {b : Prop} {c : Prop} [Decidable a] :
              ab c (ab) (ac)
              theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b] :
              ab c (ab) (ac)
              theorem Decidable.not_imp {a : Prop} {b : Prop} [Decidable a] :
              ¬(ab) a ¬b
              theorem Decidable.peirce (a : Prop) (b : Prop) [Decidable a] :
              ((ab) → a) → a
              theorem peirce' {a : Prop} (H : (b : Prop) → (ab) → a) :
              a
              theorem Decidable.not_iff_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] :
              (¬a ¬b) (a b)
              theorem Decidable.not_iff_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] :
              (¬a b) (¬b a)
              theorem Decidable.not_iff {b : Prop} {a : Prop} [Decidable b] :
              ¬(a b) (¬a b)
              theorem Decidable.iff_not_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] :
              (a ¬b) (b ¬a)
              theorem Decidable.not_and_not_right {b : Prop} {a : Prop} [Decidable b] :
              ¬(a ¬b) ab
              theorem Decidable.not_and {a : Prop} {b : Prop} [Decidable a] :
              ¬(a b) ¬a ¬b
              theorem Decidable.not_and' {b : Prop} {a : Prop} [Decidable b] :
              ¬(a b) ¬a ¬b
              theorem Decidable.imp_iff_right_iff {a : Prop} {b : Prop} [Decidable a] :
              (ab b) a b
              theorem Decidable.and_or_imp {a : Prop} {b : Prop} {c : Prop} [Decidable a] :
              a b (ac) ab c
              theorem Decidable.or_congr_left' {c : Prop} {a : Prop} {b : Prop} [Decidable c] (h : ¬c → (a b)) :
              a c b c
              theorem Decidable.or_congr_right' {a : Prop} {b : Prop} {c : Prop} [Decidable a] (h : ¬a → (b c)) :
              a b a c
              @[inline]
              def decidable_of_iff {b : Prop} (a : Prop) (h : a b) [Decidable a] :

              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 dec_trivial will not work.

              Instances For
                @[inline]
                def decidable_of_iff' {a : Prop} (b : Prop) (h : a b) [Decidable b] :

                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.

                Instances For
                  instance Decidable.predToBool {α : Sort u_1} (p : αProp) [DecidablePred p] :
                  CoeDep (αProp) p (αBool)
                  def decidable_of_bool {a : Prop} (b : Bool) :
                  (b = true a) → Decidable a

                  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.)

                  Instances For

                    classical logic #

                    theorem Classical.not_not {a : Prop} :

                    The Double Negation Theorem: ¬¬P is equivalent to P. The left-to-right direction, double negation elimination (DNE), is classically true but not constructively.

                    equality #

                    theorem heq_iff_eq :
                    ∀ {α : Sort u_1} {a b : α}, HEq a b a = b
                    theorem proof_irrel_heq {p : Prop} {q : Prop} (hp : p) (hq : q) :
                    HEq hp hq
                    @[simp]
                    theorem eq_rec_constant {α : Sort u_1} {a : α} {a' : α} {β : Sort u_2} (y : β) (h : a = a') :
                    hy = y
                    theorem congrArg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) {x : α} {x' : α} {y : β} {y' : β} (hx : x = x') (hy : y = y') :
                    f x y = f x' y'

                    membership #

                    theorem ne_of_mem_of_not_mem {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {a : α} {b : α} (h : a s) :
                    ¬b sa b
                    theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {t : β} {a : α} (h : a s) :
                    ¬a ts t

                    if-then-else #

                    @[simp]
                    theorem if_true {α : Sort u_1} {h : Decidable True} (t : α) (e : α) :
                    (if True then t else e) = t
                    @[simp]
                    theorem if_false {α : Sort u_1} {h : Decidable False} (t : α) (e : α) :
                    (if False then t else e) = e
                    theorem ite_id {c : Prop} [Decidable c] {α : Sort u_1} (t : α) :
                    (if c then t else t) = t
                    theorem apply_dite {α : Sort u_1} {β : Sort u_2} (f : αβ) (P : Prop) [Decidable P] (x : Pα) (y : ¬Pα) :
                    f (dite P x y) = if h : P then f (x h) else f (y h)

                    A function applied to a dite is a dite of that function applied to each of the branches.

                    theorem apply_ite {α : Sort u_1} {β : Sort u_2} (f : αβ) (P : Prop) [Decidable P] (x : α) (y : α) :
                    f (if P then x else y) = if P then f x else f y

                    A function applied to a ite is a ite of that function applied to each of the branches.

                    @[simp]
                    theorem dite_not {α : Sort u_1} (P : Prop) [Decidable P] (x : ¬Pα) (y : ¬¬Pα) :
                    dite (¬P) x y = dite P (fun h => y (_ : ¬¬P)) x

                    Negation of the condition P : Prop in a dite is the same as swapping the branches.

                    @[simp]
                    theorem ite_not {α : Sort u_1} (P : Prop) [Decidable P] (x : α) (y : α) :
                    (if ¬P then x else y) = if P then y else x

                    Negation of the condition P : Prop in a ite is the same as swapping the branches.

                    miscellaneous #

                    def Empty.elim {C : Sort u_1} :
                    EmptyC

                    Ex falso, the nondependent eliminator for the Empty type.

                    Instances For
                      def PEmpty.elim {C : Sort u_1} :
                      PEmptyC

                      Ex falso, the nondependent eliminator for the PEmpty type.

                      Instances For
                        instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] :
                        instance instInhabitedPSum {α : Sort u_1} {β : Sort u_2} [Inhabited α] :
                        Inhabited (α ⊕' β)
                        instance instInhabitedPSum_1 {α : Sort u_1} {β : Sort u_2} [Inhabited β] :
                        Inhabited (α ⊕' β)
                        theorem eq_iff_true_of_subsingleton {α : Sort u_1} [Subsingleton α] (x : α) (y : α) :
                        x = y True
                        theorem subsingleton_of_forall_eq {α : Sort u_1} (x : α) (h : ∀ (y : α), y = x) :

                        If all points are equal to a given point x, then α is a subsingleton.

                        theorem subsingleton_iff_forall_eq {α : Sort u_1} (x : α) :
                        Subsingleton α ∀ (y : α), y = x
                        theorem Bool.eq_iff_iff {a : Bool} {b : Bool} :
                        a = b (a = true b = true)
                        theorem ne_comm {α : Sort u_1} {a : α} {b : α} :
                        a b b a