mathlib docs: logic.basic

def hidden {α : Sort u_1} :

Π {a : α}, α

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

Equations

hidden = a

source

def empty.elim {C : Sort u_1} :

empty → C

Ex falso, the nondependent eliminator for the empty type.

source

@[instance]

def empty.subsingleton :

subsingleton empty

Equations

empty.subsingleton = _

source

@[instance]

def subsingleton.prod {α : Type u_1} {β : Type u_2} [subsingleton α] [subsingleton β] :

subsingleton (α × β)

Equations

subsingleton.prod = _

source

@[instance]

def empty.decidable_eq :

decidable_eq empty

Equations

empty.decidable_eq = λ (a : empty), a.elim

source

@[instance]

def sort.inhabited :

inhabited (Sort u_1)

Equations

sort.inhabited = {default := punit}

source

@[instance]

def sort.inhabited' :

inhabited (inhabited.default (Sort u_1))

Equations

sort.inhabited' = {default := punit.star}

source

@[instance]

def psum.inhabited_left {α : Sort u_1} {β : Sort u_2} [inhabited α] :

inhabited (psum α β)

Equations

psum.inhabited_left = {default := psum.inl (inhabited.default α)}

source

@[instance]

def psum.inhabited_right {α : Sort u_1} {β : Sort u_2} [inhabited β] :

inhabited (psum α β)

Equations

psum.inhabited_right = {default := psum.inr (inhabited.default β)}

source

@[instance]

def decidable_eq_of_subsingleton {α : Sort u_1} [subsingleton α] :

decidable_eq α

Equations

decidable_eq_of_subsingleton a b = decidable.is_true _

source

@[simp]

theorem eq_iff_true_of_subsingleton {α : Type u_1} [subsingleton α] (x y : α) :

x = y ↔ true

source

@[simp]

theorem coe_coe {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [has_coe α β] [has_coe_t β γ] (a : α) :

↑a = ↑↑a

Add an instance to "undo" coercion transitivity into a chain of coercions, because most simp lemmas are stated with respect to simple coercions and will not match when part of a chain.

source

theorem coe_fn_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_fun γ] (x : α) :

⇑x = ⇑↑x

source

@[simp]

theorem coe_fn_coe_base {α : Sort u_1} {β : Sort u_2} [has_coe α β] [has_coe_to_fun β] (x : α) :

⇑x = ⇑↑x

source

theorem coe_sort_coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [has_coe α β] [has_coe_t_aux β γ] [has_coe_to_sort γ] (x : α) :

↥x = ↥↑x

source

@[simp]

theorem coe_sort_coe_base {α : Sort u_1} {β : Sort u_2} [has_coe α β] [has_coe_to_sort β] (x : α) :

↥x = ↥↑x

source

@[instance]

def pempty.decidable_eq :

decidable_eq pempty

source

@[nolint]

constant pempty :

Sort u

pempty is the universe-polymorphic analogue of empty.

source

def pempty.elim {C : Sort u_1} :

pempty → C

Ex falso, the nondependent eliminator for the pempty type.

source

@[instance]

def subsingleton_pempty :

subsingleton pempty

Equations

subsingleton_pempty = _

source

@[simp]

theorem not_nonempty_pempty :

¬nonempty pempty

source

@[simp]

theorem forall_pempty {P : pempty → Prop} :

(∀ (x : pempty), P x) ↔ true

source

@[simp]

theorem exists_pempty {P : pempty → Prop} :

(∃ (x : pempty), P x) ↔ false

source

theorem congr_arg_heq {α : Sort u_1} {β : α → Sort u_2} (f : Π (a : α), β a) {a₁ a₂ : α} :

a₁ = a₂ → f a₁ == f a₂

source

theorem plift.down_inj {α : Sort u_1} (a b : plift α) :

a.down = b.down → a = b

source

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

a ≠ b ↔ b ≠ a

source

@[simp]

theorem eq_iff_eq_cancel_left {α : Type u_1} {b c : α} :

(∀ {a : α}, a = b ↔ a = c) ↔ b = c

source

@[simp]

theorem eq_iff_eq_cancel_right {α : Type u_1} {a b : α} :

(∀ {c : α}, a = c ↔ b = c) ↔ a = b

source

@[class]

def fact :

Prop → Prop

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

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

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

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

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

Equations

fact p = p

Instances

source

theorem false_ne_true :

false ≠ true

source

theorem iff_of_eq {a b : Prop} :

a = b → (a ↔ b)

source

theorem iff_iff_eq {a b : Prop} :

a ↔ b ↔ a = b

source

@[simp]

theorem eq_iff_iff {p q : Prop} :

p = q ↔ (p ↔ q)

source

@[simp]

theorem imp_self {a : Prop} :

a → a ↔ true

source

@[nolint]

theorem imp_intro {α β : Prop} :

α → β → α

source

theorem imp_false {a : Prop} :

a → false ↔ ¬a

source

theorem imp_and_distrib {b c : Prop} {α : Sort u_1} :

α → b ∧ c ↔ (α → b) ∧ (α → c)

source

@[simp]

theorem and_imp {a b c : Prop} :

a ∧ b → c ↔ a → b → c

source

theorem iff_def {a b : Prop} :

a ↔ b ↔ (a → b) ∧ (b → a)

source

theorem iff_def' {a b : Prop} :

a ↔ b ↔ (b → a) ∧ (a → b)

source

theorem imp_true_iff {α : Sort u_1} :

α → true ↔ true

source

@[simp]

theorem imp_iff_right {a b : Prop} :

a → (a → b ↔ b)

source

def not.elim {a : Prop} {α : Sort u_1} :

¬a → 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

H1.elim H2 = absurd H2 H1

source

theorem not.imp {a b : Prop} :

¬b → (a → b) → ¬a

source

theorem not_not_of_not_imp {a b : Prop} :

¬(a → b) → ¬¬a

source

theorem not_of_not_imp {b a : Prop} :

¬(a → b) → ¬b

source

@[nolint]

theorem dec_em (p : Prop) [decidable p] :

p ∨ ¬p

source

theorem em (p : Prop) :

p ∨ ¬p

source

theorem or_not {p : Prop} :

p ∨ ¬p

source

theorem by_contradiction {p : Prop} :

(¬p → false) → p

source

theorem by_contra {p : Prop} :

(¬p → false) → p

source

theorem decidable.not_not {a : Prop} [decidable a] :

¬¬a ↔ a

source

@[simp]

theorem not_not {a : Prop} :

¬¬a ↔ a

source

theorem of_not_not {a : Prop} :

¬¬a → a

source

theorem decidable.of_not_imp {a b : Prop} [decidable a] :

¬(a → b) → a

source

theorem of_not_imp {a b : Prop} :

¬(a → b) → a

source

theorem decidable.not_imp_symm {a b : Prop} [decidable a] :

(¬a → b) → ¬b → a

source

@[nolint]

theorem not.decidable_imp_symm {a b : Prop} [decidable a] :

(¬a → b) → ¬b → a

source

theorem not.imp_symm {a b : Prop} :

(¬a → b) → ¬b → a

source

theorem decidable.not_imp_comm {a b : Prop} [decidable a] [decidable b] :

¬a → b ↔ ¬b → a

source

theorem not_imp_comm {a b : Prop} :

¬a → b ↔ ¬b → a

source

theorem imp.swap {a b c : Prop} :

a → b → c ↔ b → a → c

source

theorem imp_not_comm {a b : Prop} :

a → ¬b ↔ b → ¬a

source

theorem not_and_of_not_left {a : Prop} (b : Prop) :

¬a → ¬(a ∧ b)

source

theorem not_and_of_not_right (a : Prop) {b : Prop} :

¬b → ¬(a ∧ b)

source

theorem and.imp_left {a b c : Prop} :

(a → b) → a ∧ c → b ∧ c

source

theorem and.imp_right {a b c : Prop} :

(a → b) → c ∧ a → c ∧ b

source

theorem and.right_comm {a b c : Prop} :

(a ∧ b) ∧ c ↔ (a ∧ c) ∧ b

source

theorem and.rotate {a b c : Prop} :

a ∧ b ∧ c ↔ b ∧ c ∧ a

source

theorem and_not_self_iff (a : Prop) :

a ∧ ¬a ↔ false

source

theorem not_and_self_iff (a : Prop) :

¬a ∧ a ↔ false

source

theorem and_iff_left_of_imp {a b : Prop} :

(a → b) → (a ∧ b ↔ a)

source

theorem and_iff_right_of_imp {a b : Prop} :

(b → a) → (a ∧ b ↔ b)

source

@[simp]

theorem and_iff_left_iff_imp {a b : Prop} :

a ∧ b ↔ a ↔ a → b

source

@[simp]

theorem and_iff_right_iff_imp {a b : Prop} :

a ∧ b ↔ b ↔ b → a

source

theorem and.congr_right_iff {a b c : Prop} :

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

source

@[simp]

theorem and_self_left {a b : Prop} :

a ∧ a ∧ b ↔ a ∧ b

source

@[simp]

theorem and_self_right {a b : Prop} :

(a ∧ b) ∧ b ↔ a ∧ b

source

theorem or.right_comm {a b c : Prop} :

(a ∨ b) ∨ c ↔ (a ∨ c) ∨ b

source

theorem or_of_or_of_imp_of_imp {a b c d : Prop} :

a ∨ b → (a → c) → (b → d) → c ∨ d

source

theorem or_of_or_of_imp_left {a b c : Prop} :

a ∨ c → (a → b) → b ∨ c

source

theorem or_of_or_of_imp_right {a b c : Prop} :

c ∨ a → (a → b) → c ∨ b

source

theorem or.elim3 {a b c d : Prop} :

a ∨ b ∨ c → (a → d) → (b → d) → (c → d) → d

source

theorem or_imp_distrib {a b c : Prop} :

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

source

theorem decidable.or_iff_not_imp_left {a b : Prop} [decidable a] :

a ∨ b ↔ ¬a → b

source

theorem or_iff_not_imp_left {a b : Prop} :

a ∨ b ↔ ¬a → b

source

theorem decidable.or_iff_not_imp_right {a b : Prop} [decidable b] :

a ∨ b ↔ ¬b → a

source

theorem or_iff_not_imp_right {a b : Prop} :

a ∨ b ↔ ¬b → a

source

theorem decidable.not_imp_not {a b : Prop} [decidable a] :

¬a → ¬b ↔ b → a

source

theorem not_imp_not {a b : Prop} :

¬a → ¬b ↔ b → a

source

theorem and_or_distrib_left {a b c : Prop} :

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

source

theorem or_and_distrib_right {a b c : Prop} :

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

source

theorem or_and_distrib_left {a b c : Prop} :

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

source

theorem and_or_distrib_right {a b c : Prop} :

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

source

@[simp]

theorem or_self_left {a b : Prop} :

a ∨ a ∨ b ↔ a ∨ b

source

@[simp]

theorem or_self_right {a b : Prop} :

(a ∨ b) ∨ b ↔ a ∨ b

source

theorem iff_of_true {a b : Prop} :

a → b → (a ↔ b)

source

theorem iff_of_false {a b : Prop} :

¬a → ¬b → (a ↔ b)

source

theorem iff_true_left {a b : Prop} :

a → (a ↔ b ↔ b)

source

theorem iff_true_right {a b : Prop} :

a → (b ↔ a ↔ b)

source

theorem iff_false_left {a b : Prop} :

¬a → (a ↔ b ↔ ¬b)

source

theorem iff_false_right {a b : Prop} :

¬a → (b ↔ a ↔ ¬b)

source

theorem decidable.not_or_of_imp {a b : Prop} [decidable a] :

(a → b) → ¬a ∨ b

source

theorem not_or_of_imp {a b : Prop} :

(a → b) → ¬a ∨ b

source

theorem decidable.imp_iff_not_or {a b : Prop} [decidable a] :

a → b ↔ ¬a ∨ b

source

theorem imp_iff_not_or {a b : Prop} :

a → b ↔ ¬a ∨ b

source

theorem decidable.imp_or_distrib {a b c : Prop} [decidable a] :

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

source

theorem imp_or_distrib {a b c : Prop} :

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

source

theorem decidable.imp_or_distrib' {a b c : Prop} [decidable b] :

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

source

theorem imp_or_distrib' {a b c : Prop} :

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

source

theorem not_imp_of_and_not {a b : Prop} :

a ∧ ¬b → ¬(a → b)

source

theorem decidable.not_imp {a b : Prop} [decidable a] :

¬(a → b) ↔ a ∧ ¬b

source

theorem not_imp {a b : Prop} :

¬(a → b) ↔ a ∧ ¬b

source

theorem imp_imp_imp {a b c d : Prop} :

(c → a) → (b → d) → (a → b) → c → d

source

theorem decidable.peirce (a b : Prop) [decidable a] :

((a → b) → a) → a

source

theorem peirce (a b : Prop) :

((a → b) → a) → a

source

theorem peirce' {a : Prop} :

(∀ (b : Prop), (a → b) → a) → a

source

theorem decidable.not_iff_not {a b : Prop} [decidable a] [decidable b] :

¬a ↔ ¬b ↔ (a ↔ b)

source

theorem not_iff_not {a b : Prop} :

¬a ↔ ¬b ↔ (a ↔ b)

source

theorem decidable.not_iff_comm {a b : Prop} [decidable a] [decidable b] :

¬a ↔ b ↔ (¬b ↔ a)

source

theorem not_iff_comm {a b : Prop} :

¬a ↔ b ↔ (¬b ↔ a)

source

theorem decidable.not_iff {a b : Prop} [decidable b] :

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

source

theorem not_iff {a b : Prop} :

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

source

theorem decidable.iff_not_comm {a b : Prop} [decidable a] [decidable b] :

a ↔ ¬b ↔ (b ↔ ¬a)

source

theorem iff_not_comm {a b : Prop} :

a ↔ ¬b ↔ (b ↔ ¬a)

source

theorem decidable.iff_iff_and_or_not_and_not {a b : Prop} [decidable b] :

a ↔ b ↔ a ∧ b ∨ ¬a ∧ ¬b

source

theorem iff_iff_and_or_not_and_not {a b : Prop} :

a ↔ b ↔ a ∧ b ∨ ¬a ∧ ¬b

source

theorem decidable.iff_iff_not_or_and_or_not {a b : Prop} [decidable a] [decidable b] :

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

source

theorem iff_iff_not_or_and_or_not {a b : Prop} :

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

source

theorem decidable.not_and_not_right {a b : Prop} [decidable b] :

¬(a ∧ ¬b) ↔ a → b

source

theorem not_and_not_right {a b : Prop} :

¬(a ∧ ¬b) ↔ a → b

source

def decidable_of_iff {b : Prop} (a : Prop) (h : a ↔ b) [D : 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 D h

source

def decidable_of_iff' {a : Prop} (b : Prop) (h : a ↔ b) [D : 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 D _

source

def decidable_of_bool {a : Prop} (b : bool) :

(↥b ↔ 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 bool.tt h = decidable.is_true _
decidable_of_bool bool.ff h = decidable.is_false _

source

theorem not_and_of_not_or_not {a b : Prop} :

¬a ∨ ¬b → ¬(a ∧ b)

source

theorem decidable.not_and_distrib {a b : Prop} [decidable a] :

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

source

theorem decidable.not_and_distrib' {a b : Prop} [decidable b] :

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

source

theorem not_and_distrib {a b : Prop} :

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

source

@[simp]

theorem not_and {a b : Prop} :

¬(a ∧ b) ↔ a → ¬b

source

theorem not_and' {a b : Prop} :

¬(a ∧ b) ↔ b → ¬a

source

theorem not_or_distrib {a b : Prop} :

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

source

theorem decidable.or_iff_not_and_not {a b : Prop} [decidable a] [decidable b] :

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

source

theorem or_iff_not_and_not {a b : Prop} :

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

source

theorem decidable.and_iff_not_or_not {a b : Prop} [decidable a] [decidable b] :

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

source

theorem and_iff_not_or_not {a b : Prop} :

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

source

@[simp]

theorem heq_iff_eq {α : Sort u_1} {a b : α} :

a == b ↔ a = b

source

theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) :

hp == hq

source

theorem ne_of_mem_of_not_mem {α : out_param (Type u_1)} {β : Type u_2} [has_mem α β] {s : β} {a b : α} :

a ∈ s → b ∉ s → a ≠ b

source

theorem eq_equivalence {α : Sort u_1} :

equivalence eq

source

@[simp]

theorem eq_rec_constant {α : Sort u_1} {a a' : α} {β : Sort u_2} (y : β) (h : a = a') :

eq.rec y h = y

Transport through trivial families is the identity.

source

@[simp]

theorem eq_mp_rfl {α : Sort u_1} {a : α} :

_.mp a = a

source

@[simp]

theorem eq_mpr_rfl {α : Sort u_1} {a : α} :

_.mpr a = a

source

theorem heq_of_eq_mp {α β : Sort u_1} {a : α} {a' : β} (e : α = β) :

e.mp a = a' → a == a'

source

theorem rec_heq_of_heq {α : Sort u_1} {a b : α} {β : Sort u_2} {C : α → Sort u_2} {x : C a} {y : β} (eq : a = b) :

x == y → _root_.eq.rec x eq == y

source

@[simp]

theorem eq_mpr_heq {α β : Sort u} (h : β = α) (x : α) :

h.mpr x == x

source

theorem eq.congr {α : Sort u_1} {x₁ x₂ y₁ y₂ : α} :

x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)

source

theorem eq.congr_left {α : Sort u_1} {x y z : α} :

x = y → (x = z ↔ y = z)

source

theorem eq.congr_right {α : Sort u_1} {x y z : α} :

x = y → (z = x ↔ z = y)

source

theorem congr_arg2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {x x' : α} {y y' : β} :

x = x' → y = y' → f x y = f x' y'

source

theorem forall_imp {α : Sort u_1} {p q : α → Prop} (h : ∀ (a : α), p a → q a) (a : ∀ (a : α), p a) (a_1 : α) :

q a_1

source

theorem Exists.imp {α : Sort u_1} {q p : α → Prop} :

(∀ (a : α), p a → q a) → (∃ (a : α), p a) → (∃ (a : α), q a)

source

theorem exists_imp_exists' {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) :

(∀ (a : α), p a → q (f a)) → (∃ (a : α), p a) → (∃ (b : β), q b)

source

theorem forall_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :

(∀ (x : α) (y : β), p x y) ↔ ∀ (y : β) (x : α), p x y

source

theorem exists_swap {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :

(∃ (x : α) (y : β), p x y) ↔ ∃ (y : β) (x : α), p x y

source

@[simp]

theorem exists_imp_distrib {α : Sort u_1} {p : α → Prop} {b : Prop} :

(∃ (x : α), p x) → b ↔ ∀ (x : α), p x → b

source

def Exists.some {α : Sort u_1} {p : α → Prop} :

(∃ (a : α), p a) → α

Extract an element from a existential statement, using classical.some.

Equations

P.some = classical.some P

source

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

p P.some

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

source

theorem not_exists_of_forall_not {α : Sort u_1} {p : α → Prop} :

(∀ (x : α), ¬p x) → (¬∃ (x : α), p x)

source

@[simp]

theorem not_exists {α : Sort u_1} {p : α → Prop} :

(¬∃ (x : α), p x) ↔ ∀ (x : α), ¬p x

source

theorem not_forall_of_exists_not {α : Sort u_1} {p : α → Prop} :

(∃ (x : α), ¬p x) → (¬∀ (x : α), p x)

source

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

(¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

source

@[simp]

theorem not_forall {α : Sort u_1} {p : α → Prop} :

(¬∀ (x : α), p x) ↔ ∃ (x : α), ¬p x

source

theorem decidable.not_forall_not {α : Sort u_1} {p : α → Prop} [decidable (∃ (x : α), p x)] :

(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

source

theorem not_forall_not {α : Sort u_1} {p : α → Prop} :

(¬∀ (x : α), ¬p x) ↔ ∃ (x : α), p x

source

theorem decidable.not_exists_not {α : Sort u_1} {p : α → Prop} [Π (x : α), decidable (p x)] :

(¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

source

@[simp]

theorem not_exists_not {α : Sort u_1} {p : α → Prop} :

(¬∃ (x : α), ¬p x) ↔ ∀ (x : α), p x

source

@[simp]

theorem forall_true_iff {α : Sort u_1} :

α → true ↔ true

source

theorem forall_true_iff' {α : Sort u_1} {p : α → Prop} :

(∀ (a : α), p a ↔ true) → ((∀ (a : α), p a) ↔ true)

source

@[simp]

theorem forall_2_true_iff {α : Sort u_1} {β : α → Sort u_2} :

(∀ (a : α), β a → true) ↔ true

source

@[simp]

theorem forall_3_true_iff {α : Sort u_1} {β : α → Sort u_2} {γ : Π (a : α), β a → Sort u_3} :

(∀ (a : α) (b : β a), γ a b → true) ↔ true

source

@[simp]

theorem forall_const {b : Prop} (α : Sort u_1) [i : nonempty α] :

α → b ↔ b

source

@[simp]

theorem exists_const {b : Prop} (α : Sort u_1) [i : nonempty α] :

(∃ (x : α), b) ↔ b

source

theorem forall_and_distrib {α : Sort u_1} {p q : α → Prop} :

(∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x

source

theorem exists_or_distrib {α : Sort u_1} {p q : α → Prop} :

(∃ (x : α), p x ∨ q x) ↔ (∃ (x : α), p x) ∨ ∃ (x : α), q x

source

@[simp]

theorem exists_and_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} :

(∃ (x : α), q ∧ p x) ↔ q ∧ ∃ (x : α), p x

source

@[simp]

theorem exists_and_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} :

(∃ (x : α), p x ∧ q) ↔ (∃ (x : α), p x) ∧ q

source

@[simp]

theorem forall_eq {α : Sort u_1} {p : α → Prop} {a' : α} :

(∀ (a : α), a = a' → p a) ↔ p a'

source

@[simp]

theorem exists_eq {α : Sort u_1} {a' : α} :

∃ (a : α), a = a'

source

@[simp]

theorem exists_eq' {α : Sort u_1} {a' : α} :

Exists (eq a')

source

@[simp]

theorem exists_eq_left {α : Sort u_1} {p : α → Prop} {a' : α} :

(∃ (a : α), a = a' ∧ p a) ↔ p a'

source

@[simp]

theorem exists_eq_right {α : Sort u_1} {p : α → Prop} {a' : α} :

(∃ (a : α), p a ∧ a = a') ↔ p a'

source

@[simp]

theorem exists_exists_and_eq_and {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : α → Prop} {q : β → Prop} :

(∃ (b : β), (∃ (a : α), p a ∧ f a = b) ∧ q b) ↔ ∃ (a : α), p a ∧ q (f a)

source

@[simp]

theorem exists_exists_eq_and {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop} :

(∃ (b : β), (∃ (a : α), f a = b) ∧ p b) ↔ ∃ (a : α), p (f a)

source

@[simp]

theorem forall_eq' {α : Sort u_1} {p : α → Prop} {a' : α} :

(∀ (a : α), a' = a → p a) ↔ p a'

source

@[simp]

theorem exists_eq_left' {α : Sort u_1} {p : α → Prop} {a' : α} :

(∃ (a : α), a' = a ∧ p a) ↔ p a'

source

@[simp]

theorem exists_eq_right' {α : Sort u_1} {p : α → Prop} {a' : α} :

(∃ (a : α), p a ∧ a' = a) ↔ p a'

source

theorem exists_comm {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} :

(∃ (a : α) (b : β), p a b) ↔ ∃ (b : β) (a : α), p a b

source

theorem forall_or_of_or_forall {α : Sort u_1} {p : α → Prop} {b : Prop} (h : b ∨ ∀ (x : α), p x) (x : α) :

b ∨ p x

source

theorem decidable.forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} [decidable q] :

(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

source

theorem forall_or_distrib_left {α : Sort u_1} {q : Prop} {p : α → Prop} :

(∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x

source

theorem decidable.forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} [decidable q] :

(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

source

theorem forall_or_distrib_right {α : Sort u_1} {q : Prop} {p : α → Prop} :

(∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q

source

theorem forall_iff_forall_surj {α : Type u_1} {β : Type u_2} {f : α → β} (h : function.surjective f) {P : β → Prop} :

(∀ (a : α), P (f a)) ↔ ∀ (b : β), P b

A predicate holds everywhere on the image of a surjective functions iff it holds everywhere.

source

@[simp]

theorem exists_prop {p q : Prop} :

(∃ (h : p), q) ↔ p ∧ q

source

@[simp]

theorem exists_false {α : Sort u_1} :

¬∃ (a : α), false

source

theorem Exists.fst {b : Prop} {p : b → Prop} :

Exists p → b

source

theorem Exists.snd {b : Prop} {p : b → Prop} (h : Exists p) :

p _

source

@[simp]

theorem forall_prop_of_true {p : Prop} {q : p → Prop} (h : p) :

(∀ (h' : p), q h') ↔ q h

source

@[simp]

theorem exists_prop_of_true {p : Prop} {q : p → Prop} (h : p) :

(∃ (h' : p), q h') ↔ q h

source

@[simp]

theorem forall_prop_of_false {p : Prop} {q : p → Prop} :

¬p → ((∀ (h' : p), q h') ↔ true)

source

@[simp]

theorem exists_prop_of_false {p : Prop} {q : p → Prop} :

¬p → (¬∃ (h' : p), q h')

source

theorem exists_unique.exists {α : Sort u_1} {p : α → Prop} :

(∃! (x : α), p x) → (∃ (x : α), p x)

source

theorem exists_unique.unique {α : Sort u_1} {p : α → Prop} (h : ∃! (x : α), p x) {y₁ y₂ : α} :

p y₁ → p y₂ → y₁ = y₂

source

@[simp]

theorem exists_unique_iff_exists {α : Sort u_1} [subsingleton α] {p : α → Prop} :

(∃! (x : α), p x) ↔ ∃ (x : α), p x

source

theorem exists_unique.elim2 {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), subsingleton (p x)] {q : Π (x : α), p x → Prop} {b : Prop} :

(∃! (x : α) (h : p x), q x h) → (∀ (x : α) (h : p x), q x h → (∀ (y : α) (hy : p y), q y hy → y = x) → b) → b

source

theorem exists_unique.intro2 {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), subsingleton (p x)] {q : Π (x : α), p x → Prop} (w : α) (hp : p w) :

q w hp → (∀ (y : α) (hy : p y), q y hy → y = w) → (∃! (x : α) (hx : p x), q x hx)

source

theorem exists_unique.exists2 {α : Sort u_1} {p : α → Sort u_2} {q : Π (x : α), p x → Prop} :

(∃! (x : α) (hx : p x), q x hx) → (∃ (x : α) (hx : p x), q x hx)

source

theorem exists_unique.unique2 {α : Sort u_1} {p : α → Sort u_2} [∀ (x : α), subsingleton (p x)] {q : Π (x : α), p x → Prop} (h : ∃! (x : α) (hx : p x), q x hx) {y₁ y₂ : α} (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) :

q y₂ hpy₂ → y₁ = y₂

source

theorem classical.cases {p : Prop → Prop} (h1 : p true) (h2 : p false) (a : Prop) :

p a

source

@[nolint]

theorem classical.dec (p : Prop) :

decidable p

source

@[nolint]

theorem classical.dec_pred {α : Sort u_1} (p : α → Prop) :

decidable_pred p

source

@[nolint]

theorem classical.dec_rel {α : Sort u_1} (p : α → α → Prop) :

decidable_rel p

source

@[nolint]

theorem classical.dec_eq (α : Sort u_1) :

decidable_eq α

source

def classical.exists_cases {α : Sort u_1} {p : α → Prop} {C : Sort u} :

C → (Π (a : α), p a → C) → C

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

Equations

classical.exists_cases H0 H = dite (∃ (a : α), p a) (λ (h : ∃ (a : α), p a), H (classical.some h) _) (λ (h : ¬∃ (a : α), p a), H0)

source

theorem classical.some_spec2 {α : Sort u_1} {p : α → Prop} {h : ∃ (a : α), p a} (q : α → Prop) :

(∀ (a : α), p a → q a) → q (classical.some h)

source

def classical.subtype_of_exists {α : Type u_1} {P : α → Prop} :

(∃ (x : α), P x) → {x // P x}

A version of classical.indefinite_description which is definitionally equal to a pair

Equations

classical.subtype_of_exists h = ⟨classical.some h, _⟩

source

def exists.classical_rec_on {α : Sort u_1} {p : α → Prop} (h : ∃ (a : α), p a) {C : Sort u} :

(Π (a : α), p a → C) → C

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

Equations

exists.classical_rec_on h H = H (classical.some h) _

source

theorem bex_def {α : Sort u_1} {p q : α → Prop} :

(∃ (x : α) (h : p x), q x) ↔ ∃ (x : α), p x ∧ q x

source

theorem bex.elim {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} {b : Prop} :

(∃ (x : α) (h : p x), P x h) → (∀ (a : α) (h : p a), P a h → b) → b

source

theorem bex.intro {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} (a : α) (h₁ : p a) :

P a h₁ → (∃ (x : α) (h : p x), P x h)

source

theorem ball_congr {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} :

(∀ (x : α) (h : p x), P x h ↔ Q x h) → ((∀ (x : α) (h : p x), P x h) ↔ ∀ (x : α) (h : p x), Q x h)

source

theorem bex_congr {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} :

(∀ (x : α) (h : p x), P x h ↔ Q x h) → ((∃ (x : α) (h : p x), P x h) ↔ ∃ (x : α) (h : p x), Q x h)

source

theorem ball.imp_right {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} (H : ∀ (x : α) (h : p x), P x h → Q x h) (h₁ : ∀ (x : α) (h : p x), P x h) (x : α) (h : p x) :

Q x h

source

theorem bex.imp_right {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} :

(∀ (x : α) (h : p x), P x h → Q x h) → (∃ (x : α) (h : p x), P x h) → (∃ (x : α) (h : p x), Q x h)

source

theorem ball.imp_left {α : Sort u_1} {r p q : α → Prop} (H : ∀ (x : α), p x → q x) (h₁ : ∀ (x : α), q x → r x) (x : α) :

p x → r x

source

theorem bex.imp_left {α : Sort u_1} {r p q : α → Prop} :

(∀ (x : α), p x → q x) → (∃ (x : α) (_x : p x), r x) → (∃ (x : α) (_x : q x), r x)

source

theorem ball_of_forall {α : Sort u_1} {p : α → Prop} (h : ∀ (x : α), p x) (x : α) :

p x

source

theorem forall_of_ball {α : Sort u_1} {p q : α → Prop} (H : ∀ (x : α), p x) (h : ∀ (x : α), p x → q x) (x : α) :

q x

source

theorem bex_of_exists {α : Sort u_1} {p q : α → Prop} :

(∀ (x : α), p x) → (∃ (x : α), q x) → (∃ (x : α) (_x : p x), q x)

source

theorem exists_of_bex {α : Sort u_1} {p q : α → Prop} :

(∃ (x : α) (_x : p x), q x) → (∃ (x : α), q x)

source

@[simp]

theorem bex_imp_distrib {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} {b : Prop} :

(∃ (x : α) (h : p x), P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b

source

theorem not_bex {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} :

(¬∃ (x : α) (h : p x), P x h) ↔ ∀ (x : α) (h : p x), ¬P x h

source

theorem not_ball_of_bex_not {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} :

(∃ (x : α) (h : p x), ¬P x h) → (¬∀ (x : α) (h : p x), P x h)

source

theorem decidable.not_ball {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} [decidable (∃ (x : α) (h : p x), ¬P x h)] [Π (x : α) (h : p x), decidable (P x h)] :

(¬∀ (x : α) (h : p x), P x h) ↔ ∃ (x : α) (h : p x), ¬P x h

source

theorem not_ball {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} :

(¬∀ (x : α) (h : p x), P x h) ↔ ∃ (x : α) (h : p x), ¬P x h

source

theorem ball_true_iff {α : Sort u_1} (p : α → Prop) :

(∀ (x : α), p x → true) ↔ true

source

theorem ball_and_distrib {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} :

(∀ (x : α) (h : p x), P x h ∧ Q x h) ↔ (∀ (x : α) (h : p x), P x h) ∧ ∀ (x : α) (h : p x), Q x h

source

theorem bex_or_distrib {α : Sort u_1} {p : α → Prop} {P Q : Π (x : α), p x → Prop} :

(∃ (x : α) (h : p x), P x h ∨ Q x h) ↔ (∃ (x : α) (h : p x), P x h) ∨ ∃ (x : α) (h : p x), Q x h

source

theorem classical.not_ball {α : Sort u_1} {p : α → Prop} {P : Π (x : α), p x → Prop} :

(¬∀ (x : α) (h : p x), P x h) ↔ ∃ (x : α) (h : p x), ¬P x h

source

theorem ite_eq_iff {α : Sort u_1} {p : Prop} [decidable p] {a b c : α} :

ite p a b = c ↔ p ∧ a = c ∨ ¬p ∧ b = c

source

@[instance]

def has_zero.nonempty {α : Type u} [has_zero α] :

nonempty α

Equations

has_zero.nonempty = _

source

@[instance]

def has_one.nonempty {α : Type u} [has_one α] :

nonempty α

Equations

has_one.nonempty = _

source

theorem exists_true_iff_nonempty {α : Sort u_1} :

(∃ (a : α), true) ↔ nonempty α

source

@[simp]

theorem nonempty_Prop {p : Prop} :

nonempty p ↔ p

source

theorem not_nonempty_iff_imp_false {α : Type u} :

¬nonempty α ↔ α → false

source

@[simp]

theorem nonempty_sigma {α : Type u} {γ : α → Type w} :

nonempty (Σ (a : α), γ a) ↔ ∃ (a : α), nonempty (γ a)

source

@[simp]

theorem nonempty_subtype {α : Sort u} {p : α → Prop} :

nonempty (subtype p) ↔ ∃ (a : α), p a

source

@[simp]

theorem nonempty_prod {α : Type u} {β : Type v} :

nonempty (α × β) ↔ nonempty α ∧ nonempty β

source

@[simp]

theorem nonempty_pprod {α : Sort u} {β : Sort v} :

nonempty (pprod α β) ↔ nonempty α ∧ nonempty β

source

@[simp]

theorem nonempty_sum {α : Type u} {β : Type v} :

nonempty (α ⊕ β) ↔ nonempty α ∨ nonempty β

source

@[simp]

theorem nonempty_psum {α : Sort u} {β : Sort v} :

nonempty (psum α β) ↔ nonempty α ∨ nonempty β

source

@[simp]

theorem nonempty_psigma {α : Sort u} {β : α → Sort v} :

nonempty (psigma β) ↔ ∃ (a : α), nonempty (β a)

source

@[simp]

theorem nonempty_empty :

¬nonempty empty

source

@[simp]

theorem nonempty_ulift {α : Type u} :

nonempty (ulift α) ↔ nonempty α

source

@[simp]

theorem nonempty_plift {α : Sort u} :

nonempty (plift α) ↔ nonempty α

source

@[simp]

theorem nonempty.forall {α : Sort u} {p : nonempty α → Prop} :

(∀ (h : nonempty α), p h) ↔ ∀ (a : α), p _

source

@[simp]

theorem nonempty.exists {α : Sort u} {p : nonempty α → Prop} :

(∃ (h : nonempty α), p h) ↔ ∃ (a : α), p _

source

theorem classical.nonempty_pi {α : Sort u} {β : α → Sort v} :

nonempty (Π (a : α), β a) ↔ ∀ (a : α), nonempty (β a)

source

def classical.inhabited_of_nonempty' {α : Sort u} [h : nonempty α] :

inhabited α

Using classical.choice, lifts a (Prop-valued) nonempty instance to a (Type-valued) inhabited instance. classical.inhabited_of_nonempty already exists, in core/init/classical.lean, but the assumption is not a type class argument, which makes it unsuitable for some applications.

Equations