More basic logic properties #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A few more logic lemmas. These are in their own file, rather than logic.basic, because it is convenient to be able to use the split_ifs tactic.

Implementation notes #

We spell those lemmas out with dite and ite rather than the if then else notation because this would result in less delta-reduced statements.

source

@[protected]

theorem heq.eq {α : Sort u_1} {a b : α} :

a == b → a = b

Alias of the forward direction of heq_iff_eq.

source

@[protected]

theorem eq.heq {α : Sort u_1} {a b : α} :

a = b → a == b

Alias of the reverse direction of heq_iff_eq.

source

theorem eq.trans_ne {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) :

a ≠ c

Alias of ne_of_eq_of_ne.

source

theorem ne.trans_eq {α : Sort u} {a b c : α} (h₁ : a ≠ b) (h₂ : b = c) :

a ≠ c

Alias of ne_of_ne_of_eq.

source

theorem dite_dite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :

dite p a (λ (hp : ¬p), dite q (b hp) (c hp)) = dite q (λ (hq : q), dite p a (λ (hp : ¬p), b hp hq)) (λ (hq : ¬q), dite p a (λ (hp : ¬p), c hp hq))

source

theorem dite_dite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} :

dite p (λ (hp : p), dite q (a hp) (b hp)) c = dite q (λ (hq : q), dite p (λ (hp : p), a hp hq) c) (λ (hq : ¬q), dite p (λ (hp : p), b hp hq) c)

source

theorem ite_dite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : α} {b : q → α} {c : ¬q → α} :

ite p a (dite q b c) = dite q (λ (hq : q), ite p a (b hq)) (λ (hq : ¬q), ite p a (c hq))

source

theorem ite_dite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : q → α} {b : ¬q → α} {c : α} :

ite p (dite q a b) c = dite q (λ (hq : q), ite p (a hq) c) (λ (hq : ¬q), ite p (b hq) c)

source

theorem dite_ite_distrib_left {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a : p → α} {b c : ¬p → α} :

dite p a (λ (hp : ¬p), ite q (b hp) (c hp)) = ite q (dite p a b) (dite p a c)

source

theorem dite_ite_distrib_right {α : Sort u_1} {p q : Prop} [decidable p] [decidable q] {a b : p → α} {c : ¬p → α} :

dite p (λ (hp : p), ite q (a hp) (b hp)) c = ite q (dite p a c) (dite p b c)

source

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

ite p a (ite q b c) = ite q (ite p a b) (ite p a c)

source

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

ite p (ite q a b) c = ite q (ite p a c) (ite p b c)

source

theorem Prop.forall {f : Prop → Prop} :

(∀ (p : Prop), f p) ↔ f true ∧ f false

source

theorem Prop.exists {f : Prop → Prop} :

(∃ (p : Prop), f p) ↔ f true ∨ f false