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

Equations

• instDecidablePredCompProp = inferInstanceAs (DecidablePred fun x => p (f x))

not

theorem Not.intro {a : Prop} (h : a → False) : ¬a

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.

Equations

• Not.elim H1 H2 = absurd H2 H1

theorem Not.imp {a : Prop} {b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a

theorem not_congr {a : Prop} {b : Prop} (h : a ↔ b) : ¬a ↔ ¬b

theorem not_not_not {a : Prop} : ¬¬¬a ↔ ¬a

theorem not_not_of_not_imp {a : Prop} {b : Prop} : ¬(a → b) → ¬¬a

theorem not_of_not_imp {b : Prop} {a : Prop} : ¬(a → b) → ¬b

@[simp]

theorem imp_not_self {a : Prop} : a → ¬a ↔ ¬a

iff

instance instTransPropIff : Trans Iff Iff Iff

Equations

• instTransPropIff = { trans := (_ : ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)) }

theorem iff_def {a : Prop} {b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a)

theorem iff_def' {a : Prop} {b : Prop} : (a ↔ b) ↔ (b → a) ∧ (a → b)

def Iff.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : (a → b) → (b → a) → α) (h : a ↔ b) : α

Non-dependent eliminator for Iff.

Equations

• Iff.elim f h = f h.mp h.mpr

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) : a ↔ True

theorem iff_false_intro {a : Prop} (h : ¬a) : a ↔ False

theorem not_iff_false_intro {a : Prop} (h : a) : ¬a ↔ False

theorem iff_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : (a ↔ b) ↔ (c ↔ d)

@[simp]

theorem not_true : ¬True ↔ False

theorem not_false_iff : ¬False ↔ True

theorem ne_self_iff_false {α : Sort u_1} (a : α) : a ≠ a ↔ False

theorem eq_self_iff_true {α : Sort u_1} (a : α) : a = a ↔ True

theorem heq_self_iff_true {α : Sort u_1} (a : α) : HEq a a ↔ True

theorem iff_not_self {a : Prop} : ¬(a ↔ ¬a)

@[simp]

theorem not_iff_self {a : Prop} : ¬(¬a ↔ a)

theorem true_iff_false : (True ↔ False) ↔ False

theorem false_iff_true : (False ↔ True) ↔ False

theorem false_of_true_iff_false : (True ↔ False) → False

theorem false_of_true_eq_false : True = False → False

theorem true_eq_false_of_false : False → True = False

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₀ : c → a) (h₁ : b → d) : (a → b) → c → d

theorem imp_iff_right {b : Prop} {a : Prop} (ha : a) : a → b ↔ b

theorem imp_true_iff (α : Sort u) : α → True ↔ True

theorem false_imp_iff (a : Prop) : False → a ↔ True

theorem true_imp_iff (α : Prop) : True → α ↔ α

@[simp]

theorem imp_self {a : Prop} : a → a ↔ True

theorem imp_false {a : Prop} : a → False ↔ ¬a

theorem imp.swap {a : Sort u_1} {b : Sort u_2} {c : Prop} : a → b → c ↔ b → a → c

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) : a → c ↔ b → c

theorem imp_congr_right {a : Sort u_1} {b : Prop} {c : Prop} (h : a → (b ↔ c)) : a → b ↔ a → c

theorem imp_congr_ctx {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : a → b ↔ c → d

theorem imp_congr {a : Prop} {c : Prop} {b : Prop} {d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a → b ↔ c → d

theorem imp_iff_not {b : Prop} {a : Prop} (hb : ¬b) : a → b ↔ ¬a

and

@[inline, reducible]

abbrev And.elim {a : Prop} {b : Prop} {α : Sort u_1} (f : a → b → α) (h : a ∧ b) : α

Non-dependent eliminator for And.

Equations

• And.elim f h = f h.left h.right

theorem And.symm {a : Prop} {b : Prop} : a ∧ b → b ∧ a

theorem And.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : a → c) (g : b → d) (h : a ∧ b) : c ∧ d

theorem And.imp_left {a : Prop} {b : Prop} {c : Prop} (h : a → b) : a ∧ c → b ∧ c

theorem And.imp_right {a : Prop} {b : Prop} {c : Prop} (h : a → b) : c ∧ a → c ∧ 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 : a → b = c) : (a ∧ b) = (a ∧ c)

theorem and_congr_left_eq {c : Prop} {a : Prop} {b : Prop} (h : c → a = 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 : a → b) : a ∧ b ↔ a

theorem and_iff_right_of_imp {b : Prop} {a : Prop} (h : b → a) : 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) ↔ a → b

@[simp]

theorem and_iff_right_iff_imp {a : Prop} {b : Prop} : (a ∧ b ↔ b) ↔ b → a

@[simp]

theorem iff_self_and {p : Prop} {q : Prop} : (p ↔ p ∧ q) ↔ p → q

@[simp]

theorem iff_and_self {p : Prop} {q : Prop} : (p ↔ q ∧ p) ↔ p → q

@[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)

theorem and_not_self_iff (a : Prop) : a ∧ ¬a ↔ False

theorem not_and_self_iff (a : Prop) : ¬a ∧ a ↔ False

or

theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a)

theorem Or.symm {a : Prop} {b : Prop} : a ∨ b → b ∨ a

theorem Or.imp {a : Prop} {c : Prop} {b : Prop} {d : Prop} (f : a → c) (g : b → d) (h : a ∨ b) : c ∨ d

theorem Or.imp_left {a : Prop} {b : Prop} {c : Prop} (f : a → b) : a ∨ c → b ∨ c

theorem Or.imp_right {b : Prop} {c : Prop} {a : Prop} (f : b → c) : a ∨ b → a ∨ 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 : a → b) : a ∨ b ↔ b

theorem or_iff_left_of_imp {b : Prop} {a : Prop} (hb : b → a) : 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) ↔ b → a

@[simp]

theorem or_iff_right_iff_imp {a : Prop} {b : Prop} : (a ∨ b ↔ b) ↔ a → b

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 → ¬(a → b)

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 ∧ b → c ↔ a → b → c

@[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 ∨ b → c ↔ (a → c) ∧ (b → c)

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 a → q 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 a → q a) : (∃ a, p a) → ∃ a, q a

theorem Exists.imp' {α : Sort u_2} {p : α → Prop} {β : Sort u_1} {q : β → Prop} (f : α → β) (hpq : (a : α) → p a → q (f a)) : (∃ a, p a) → ∃ b, q b

theorem exists_imp {α : Sort u_1} {p : α → Prop} {b : Prop} : (∃ x, p x) → b ↔ (x : α) → p x → b

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 : α) → β a → Prop} {q : (a : α) → β a → Prop} (h : ∀ (a : α) (b : β a), p a b ↔ q a b) : ((a : α) → (b : β a) → p a b) ↔ (a : α) → (b : β a) → q a b

theorem exists₂_congr {α : Sort u_1} {β : α → Sort u_2} {p : (a : α) → β a → Prop} {q : (a : α) → β a → Prop} (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 : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {q : (a : α) → (b : β a) → γ a b → Prop} (h : ∀ (a : α) (b : β a) (c : γ a b), p a b c ↔ q a b c) : ((a : α) → (b : β a) → (c : γ a b) → p a b c) ↔ (a : α) → (b : β a) → (c : γ a b) → q a b c

theorem exists₃_congr {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {p : (a : α) → (b : β a) → γ a b → Prop} {q : (a : α) → (b : β a) → γ a b → Prop} (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 : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} (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 : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {p : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} {q : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Prop} (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 : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} (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 : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {ε : (a : α) → (b : β a) → (c : γ a b) → δ a b c → Sort u_5} {p : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} {q : (a : α) → (b : β a) → (c : γ a b) → (d : δ a b c) → ε a b c d → Prop} (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.

Equations

• Exists.choose P = Classical.choose P

theorem Exists.choose_spec {α : Sort u_1} {p : α → Prop} (P : ∃ a, p a) : p (Exists.choose P)

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' = a → p 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 a → p a) ↔ p a' ∧ ((a : α) → q a → p 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 : p → Prop} (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.not_not {p : Prop} [Decidable p] : ¬¬p ↔ p

theorem Decidable.by_contra {p : Prop} [Decidable p] : (¬p → False) → 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.

Equations

• Or.by_cases h h₁ h₂ = if hp : p then h₁ hp else h₂ (Or.resolve_left h hp)

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.

Equations

• Or.by_cases' h h₁ h₂ = if hq : q then h₂ hq else h₁ (Or.resolve_right h hq)

instance exists_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] : Decidable (∃ h, P h)

Equations

• exists_prop_decidable P = if h : p then decidable_of_decidable_of_iff (_ : P h ↔ ∃ h, P h) else isFalse (_ : (∃ h, P h) → False)

instance forall_prop_decidable {p : Prop} (P : p → Prop) [Decidable p] [(h : p) → Decidable (P h)] : Decidable ((h : p) → P h)

Equations

• forall_prop_decidable P = if h : p then decidable_of_decidable_of_iff (_ : P h ↔ (h : p) → P h) else isTrue (forall_prop_decidable.proof_2 P h)

theorem decide_eq_true_iff (p : Prop) [Decidable p] : decide p = true ↔ p

@[simp]

theorem decide_eq_false_iff_not (p : Prop) [Decidable p] : decide p = false ↔ ¬p

@[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 : ¬(a → b)) : a

theorem Decidable.not_imp_symm {a : Prop} {b : Prop} [Decidable a] (h : ¬a → b) (hb : ¬b) : a

theorem Decidable.not_imp_comm {a : Prop} {b : Prop} [Decidable a] [Decidable b] : ¬a → b ↔ ¬b → a

theorem Decidable.not_imp_self {a : Prop} [Decidable a] : ¬a → a ↔ a

theorem Decidable.or_iff_not_imp_left {a : Prop} {b : Prop} [Decidable a] : a ∨ b ↔ ¬a → b

theorem Decidable.or_iff_not_imp_right {b : Prop} {a : Prop} [Decidable b] : a ∨ b ↔ ¬b → a

theorem Decidable.not_imp_not {a : Prop} {b : Prop} [Decidable a] : ¬a → ¬b ↔ b → a

theorem Decidable.not_or_of_imp {a : Prop} {b : Prop} [Decidable a] (h : a → b) : ¬a ∨ b

theorem Decidable.imp_iff_not_or {a : Prop} {b : Prop} [Decidable a] : a → b ↔ ¬a ∨ b

theorem Decidable.imp_iff_or_not {b : Prop} {a : Prop} [Decidable b] : b → a ↔ a ∨ ¬b

theorem Decidable.imp_or {a : Prop} {b : Prop} {c : Prop} [Decidable a] : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem Decidable.imp_or' {b : Prop} {a : Sort u_1} {c : Prop} [Decidable b] : a → b ∨ c ↔ (a → b) ∨ (a → c)

theorem Decidable.not_imp {a : Prop} {b : Prop} [Decidable a] : ¬(a → b) ↔ a ∧ ¬b

theorem Decidable.peirce (a : Prop) (b : Prop) [Decidable a] : ((a → b) → a) → a

theorem peirce' {a : Prop} (H : (b : Prop) → (a → b) → 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.iff_iff_and_or_not_and_not {b : Prop} {a : Prop} [Decidable b] : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b

theorem Decidable.iff_iff_not_or_and_or_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

theorem Decidable.not_and_not_right {b : Prop} {a : Prop} [Decidable b] : ¬(a ∧ ¬b) ↔ a → b

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.or_iff_not_and_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : a ∨ b ↔ ¬(¬a ∧ ¬b)

theorem Decidable.and_iff_not_or_not {a : Prop} {b : Prop} [Decidable a] [Decidable b] : a ∧ b ↔ ¬(¬a ∨ ¬b)

theorem Decidable.imp_iff_right_iff {a : Prop} {b : Prop} [Decidable a] : (a → b ↔ b) ↔ a ∨ b

theorem Decidable.and_or_imp {a : Prop} {b : Prop} {c : Prop} [Decidable a] : a ∧ b ∨ (a → c) ↔ a → b ∨ 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] : Decidable b

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.

Equations

• decidable_of_iff a h = decidable_of_decidable_of_iff h

@[inline]

def decidable_of_iff' {a : Prop} (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a

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.

Equations

• decidable_of_iff' b h = decidable_of_decidable_of_iff (_ : b ↔ a)

instance Decidable.predToBool {α : Sort u_1} (p : α → Prop) [DecidablePred p] : CoeDep (α → Prop) p (α → Bool)

Equations

• Decidable.predToBool p = { coe := fun b => decide (p b) }

theorem Bool.ff_ne_tt : false ≠ true

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

Equations

• decidable_of_bool x x = match x, x with | true, h => isTrue (decidable_of_bool.proof_1 h) | false, h => isFalse (_ : ¬a)

classical logic

theorem Classical.not_not {a : Prop} : ¬¬a ↔ a

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') : h ▸ y = 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 ∈ s → a ≠ b

theorem ne_of_mem_of_not_mem' {α : Type u_1} {β : Type u_2} [Membership α β] {s : β} {t : β} {a : α} (h : a ∈ s) : ¬a ∈ t → s ≠ 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} : Empty → C

Ex falso, the nondependent eliminator for the Empty type.

Equations

• Empty.elim a = nomatch a

instance instSubsingletonEmpty : Subsingleton Empty

Equations

• instSubsingletonEmpty = instSubsingletonEmpty.proof_1

instance instDecidableEqEmpty : DecidableEq Empty

Equations

• instDecidableEqEmpty a = Empty.elim a

def PEmpty.elim {C : Sort u_1} : PEmpty → C

Ex falso, the nondependent eliminator for the PEmpty type.

Equations

• PEmpty.elim a = nomatch a

instance instSubsingletonPEmpty : Subsingleton PEmpty

Equations

• instSubsingletonPEmpty = instSubsingletonPEmpty.proof_1

instance instDecidableEqPEmpty : DecidableEq PEmpty

Equations

• instDecidableEqPEmpty a = PEmpty.elim a

@[simp]

theorem not_nonempty_empty : ¬Nonempty Empty

@[simp]

theorem not_nonempty_pempty : ¬Nonempty PEmpty

instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] : Subsingleton (α × β)

Equations

• @instSubsingletonProd = @instSubsingletonProd.proof_1

instance instInhabitedSort_1 : Inhabited (Sort u_1)

Equations

• instInhabitedSort_1 = { default := PUnit }

instance instInhabitedDefaultSortInstInhabitedSort_1 : Inhabited default

Equations

• instInhabitedDefaultSortInstInhabitedSort_1 = { default := PUnit.unit }

instance instInhabitedPSum {α : Sort u_1} {β : Sort u_2} [Inhabited α] : Inhabited (α ⊕' β)

Equations

• instInhabitedPSum = { default := PSum.inl default }

instance instInhabitedPSum_1 {α : Sort u_1} {β : Sort u_2} [Inhabited β] : Inhabited (α ⊕' β)

Equations

• instInhabitedPSum_1 = { default := PSum.inr default }

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) : Subsingleton α

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 false_ne_true : False ≠ True

theorem Bool.eq_false_or_eq_true (b : Bool) : b = true ∨ b = false

theorem Bool.eq_false_iff {b : Bool} : b = false ↔ b ≠ true

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