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

theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β) : f ∘ g = fun (x : α) => f (g 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 (_ : a → b) (_ : b → a)

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)

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 (_ : a) (_ : b)

theorem and_self_iff {a : Prop} : a ∧ a ↔ a

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_self_iff {a : Prop} : a ∨ 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

@[simp]

theorem exists_const {b : Prop} (α : Sort u_1) [i : Nonempty α] : (∃ (x : α), b) ↔ 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 : β a), p a b) ↔ ∃ (a : α), ∃ (b : β a), 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 : β a), ∃ (c : γ a b), p a b c) ↔ ∃ (a : α), ∃ (b : β a), ∃ (c : γ a b), 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 : β 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 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 : β 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

@[simp]

theorem not_exists {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x

theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} : (∀ (x : α), ¬p x) → ¬∃ (x : α), p x

Alias of the reverse direction of not_exists.

theorem forall_not_of_not_exists {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), p x) → ∀ (x : α), ¬p x

Alias of the forward direction of not_exists.

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} {q : α → Prop} {a' : α} : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a'

@[simp]

theorem exists_eq_right_right' {α : Sort u_1} {p : α → Prop} {q : α → Prop} {a' : α} : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a'

@[simp]

theorem exists_prop {b : Prop} {a : Prop} : (∃ (_h : a), 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

@[simp]

theorem forall_apply_eq_imp_iff {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop} : (∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)

@[simp]

theorem forall_eq_apply_imp_iff {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : β → Prop} : (∀ (b : β) (a : α), b = f a → p b) ↔ ∀ (a : α), p (f a)

@[simp]

theorem forall_apply_eq_imp_iff₂ {α : Sort u_2} {β : Sort u_1} {f : α → β} {p : α → Prop} {q : β → Prop} : (∀ (b : β) (a : α), p a → f a = b → q b) ↔ ∀ (a : α), p a → q (f a)

theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ (h' : p), q h') ↔ True

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₂ (_ : q)

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₁ (_ : p)

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

Equations

• exists_prop_decidable P = if h : p then decidable_of_decidable_of_iff (_ : P h ↔ ∃ (h : p), P h) else isFalse (_ : (∃ (h : p), 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 (_ : ∀ (h2 : p), P h2)

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

@[simp]

theorem decide_eq_false_iff_not (p : Prop) : ∀ {x : Decidable p}, decide p = false ↔ ¬p

@[simp]

theorem decide_eq_decide {p : Prop} {q : Prop} : ∀ {x : Decidable p} {x_1 : 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 {a : Prop} {b : 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) }

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 (_ : a) | false, h => isFalse (_ : ¬a)

theorem Decidable.not_forall {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Decidable.exists_not_of_not_forall {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), ¬p x)] [(x : α) → Decidable (p x)] : (¬∀ (x : α), p x) → ∃ (x : α), ¬p x

Alias of the forward direction of Decidable.not_forall.

theorem Decidable.not_forall_not {α : Sort u_1} {p : α → Prop} [Decidable (∃ (x : α), p x)] : (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

theorem Decidable.not_exists_not {α : Sort u_1} {p : α → Prop} [(x : α) → Decidable (p x)] : (¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

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.

@[simp]

theorem Classical.not_forall {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

theorem Classical.exists_not_of_not_forall {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), p x) → ∃ (x : α), ¬p x

Alias of the forward direction of Classical.not_forall.

theorem Classical.not_forall_not {α : Sort u_1} {p : α → Prop} : (¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

theorem Classical.not_exists_not {α : Sort u_1} {p : α → Prop} : (¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

theorem Classical.forall_or_exists_not {α : Sort u_1} (P : α → Prop) : (∀ (a : α), P a) ∨ ∃ (a : α), ¬P a

theorem Classical.exists_or_forall_not {α : Sort u_1} (P : α → Prop) : (∃ (a : α), P a) ∨ ∀ (a : α), ¬P a

theorem Classical.or_iff_not_imp_left {a : Prop} {b : Prop} : a ∨ b ↔ ¬a → b

theorem Classical.or_iff_not_imp_right {a : Prop} {b : Prop} : a ∨ b ↔ ¬b → a

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'

theorem congrFun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b

theorem congrFun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) : f a b c = g a b c

theorem funext₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : ∀ (a : α) (b : β a), f a b = g a b) : f = g

theorem funext₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c) : f = g

theorem ne_of_apply_ne {α : Sort u_1} {β : Sort u_2} (f : α → β) {x : α} {y : α} : f x ≠ f y → x ≠ y

theorem Eq.congr : ∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)

theorem Eq.congr_left {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) : x = z ↔ y = z

theorem Eq.congr_right {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) : z = x ↔ z = y

theorem congr_arg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂

Alias of congrArg.

---

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

theorem congr_arg₂ {α : 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'

Alias of congrArg₂.

theorem congr_fun {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : f = g) (a : α) : f a = g a

Alias of congrFun.

---

Congruence in the function part of an application: If f = g then f a = g a.

theorem congr_fun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) : f a b = g a b

Alias of congrFun₂.

theorem congr_fun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) : f a b c = g a b c

Alias of congrFun₃.

theorem eq_mp_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : Eq.mp h = cast h

theorem eq_mpr_eq_cast {α : Sort u_1} {β : Sort u_1} (h : α = β) : Eq.mpr h = cast (_ : β = α)

@[simp]

theorem cast_cast {α : Sort u_1} {β : Sort u_1} {γ : Sort u_1} (ha : α = β) (hb : β = γ) (a : α) : cast hb (cast ha a) = cast (_ : α = γ) a

theorem heq_of_cast_eq {α : Sort u_1} {β : Sort u_1} {a : α} {a' : β} (e : α = β) : cast e a = a' → HEq a a'

theorem cast_eq_iff_heq : ∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ HEq a_2 a'

theorem eqRec_eq_cast {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') : e ▸ x = cast (_ : motive a (_ : a = a) = motive a' e) x

theorem eqRec_heq_self {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') : HEq (e ▸ x) x

@[simp]

theorem eqRec_heq_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') {β : Sort u_2} (y : β) : HEq (e ▸ x) y ↔ HEq x y

@[simp]

theorem heq_eqRec_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a (_ : a = a)) {a' : α} (e : a = a') {β : Sort u_2} (y : β) : HEq y (e ▸ x) ↔ HEq y x

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) : ∀ {x : Decidable P} (x_1 : ¬P → α) (y : ¬¬P → α), dite (¬P) x_1 y = dite P (fun (h : P) => y (_ : ¬¬P)) x_1

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) : ∀ {x : Decidable P} (x_1 y : α), (if ¬P then x_1 else y) = if P then y else x_1

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

@[simp]

theorem dite_eq_left_iff {α : Sort u_1} {a : α} {P : Prop} [Decidable P] {B : ¬P → α} : dite P (fun (x : P) => a) B = a ↔ ∀ (h : ¬P), B h = a

@[simp]

theorem dite_eq_right_iff {α : Sort u_1} {b : α} {P : Prop} [Decidable P] {A : P → α} : (dite P A fun (x : ¬P) => b) = b ↔ ∀ (h : P), A h = b

@[simp]

theorem ite_eq_left_iff : ∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = a ↔ ¬P → b = a

@[simp]

theorem ite_eq_right_iff : ∀ {α : Sort u_1} {a b : α} {P : Prop} [inst : Decidable P], (if P then a else b) = b ↔ P → a = b

@[simp]

theorem dite_eq_ite {P : Prop} : ∀ {α : Sort u_1} {a b : α} [inst : Decidable P], (if x : P then a else b) = if P then a else b

A dite whose results do not actually depend on the condition may be reduced to an ite.

theorem ite_some_none_eq_none {P : Prop} : ∀ {α : Type u_1} {x : α} [inst : Decidable P], (if P then some x else none) = none ↔ ¬P

@[simp]

theorem ite_some_none_eq_some {P : Prop} : ∀ {α : Type u_1} {x y : α} [inst : Decidable P], (if P then some x else none) = some y ↔ P ∧ x = y

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 = (_ : Subsingleton Empty)

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 = (_ : Subsingleton PEmpty)

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

• (_ : Subsingleton (α × β)) = (_ : Subsingleton (α × β))

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_iff_iff {a : Bool} {b : Bool} : a = b ↔ (a = true ↔ b = true)

theorem ne_comm {α : Sort u_1} {a : α} {b : α} : a ≠ b ↔ b ≠ a

theorem congr_eqRec {α : Sort u_1} {γ : Sort u_2} {x : α} {x' : α} {β : α → Sort u_3} (f : (x : α) → β x → γ) (h : x = x') (y : β x) : f x' (h ▸ y) = f x y