# Documentation

Mathlib.Init.Logic

@[deprecated]
def Implies (a : Prop) (b : Prop) :
Instances For
@[deprecated]
theorem Implies.trans {p : Prop} {q : Prop} {r : Prop} (h₁ : pq) (h₂ : qr) :
pr

Implication → is transitive. If P → Q and Q → R then P → R.

@[deprecated]
Instances For
theorem proof_irrel {a : Prop} (h₁ : a) (h₂ : a) :
h₁ = h₂

Alias of proofIrrel.

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

@[deprecated]
theorem trans_rel_left {α : Sort u} {a : α} {b : α} {c : α} (r : ααProp) (h₁ : r a b) (h₂ : b = c) :
r a c
@[deprecated]
theorem trans_rel_right {α : Sort u} {a : α} {b : α} {c : α} (r : ααProp) (h₁ : a = b) (h₂ : r b c) :
r a c
theorem not_of_eq_false {p : Prop} (h : ) :
theorem cast_proof_irrel {α : Sort u_1} {β : Sort u_1} (h₁ : α = β) (h₂ : α = β) (a : α) :
cast h₁ a = cast h₂ a
theorem Ne.def {α : Sort u} (a : α) (b : α) :
(a b) = ¬a = b
theorem eq_rec_heq {α : Sort u} {φ : αSort v} {a : α} {a' : α} (h : a = a') (p : φ a) :
HEq (Eq.recOn h p) p

Alias of eqRec_heq.

theorem heq_of_eq_rec_left {α : Sort u_1} {φ : αSort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : ep₁ = p₂) :
HEq p₁ p₂
theorem heq_of_eq_rec_right {α : Sort u_1} {φ : αSort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = ep₂) :
HEq p₁ p₂
theorem of_heq_true {a : Prop} (h : ) :
a
theorem eq_rec_compose {α : Sort u} {β : Sort u} {φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α) :
Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn (_ : α = φ) a
def Xor' (a : Prop) (b : Prop) :
Instances For
theorem not_of_not_not_not {a : Prop} :
¬¬¬a¬a

Alias of the forward direction of not_not_not.

@[deprecated and_comm]
theorem and_comm' (a : Prop) (b : Prop) :
a b b a
@[deprecated and_assoc]
theorem and_assoc' {c : Prop} (a : Prop) (b : Prop) :
(a b) c a b c
theorem and_true_iff (p : Prop) :
p
theorem true_and_iff (p : Prop) :
p
theorem and_self_iff (p : Prop) :
p p p
@[deprecated or_comm]
theorem or_comm' (a : Prop) (b : Prop) :
a b b a
@[deprecated or_assoc]
theorem or_assoc' {c : Prop} (a : Prop) (b : Prop) :
(a b) c a b c
theorem true_or_iff (p : Prop) :
theorem or_true_iff (p : Prop) :
theorem false_or_iff (p : Prop) :
p
theorem or_false_iff (p : Prop) :
p
theorem or_self_iff (p : Prop) :
p p p
theorem not_or_of_not {a : Prop} {b : Prop} :
¬a¬b¬(a b)
theorem iff_true_iff {a : Prop} :
() a
theorem true_iff_iff {a : Prop} :
() a
theorem iff_false_iff {a : Prop} :
() ¬a
theorem false_iff_iff {a : Prop} :
() ¬a
theorem iff_self_iff (a : Prop) :
(a a) True
def ExistsUnique {α : Sort u_1} (p : αProp) :
Instances For
Instances For

Pretty-printing for ExistsUnique, following the same pattern as pretty printing for Exists.

Instances For
theorem ExistsUnique.intro {α : Sort u_1} {p : αProp} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p yy = w) :
∃! x, p x
theorem ExistsUnique.elim {α : Sort u} {p : αProp} {b : Prop} (h₂ : ∃! x, p x) (h₁ : (x : α) → p x(∀ (y : α), p yy = x) → b) :
b
theorem exists_unique_of_exists_of_unique {α : Sort u} {p : αProp} (hex : x, p x) (hunique : ∀ (y₁ y₂ : α), p y₁p y₂y₁ = y₂) :
∃! x, p x
theorem ExistsUnique.exists {α : Sort u_1} {p : αProp} :
(∃! x, p x) → x, p x
theorem ExistsUnique.unique {α : Sort u} {p : αProp} (h : ∃! x, p x) {y₁ : α} {y₂ : α} (py₁ : p y₁) (py₂ : p y₂) :
y₁ = y₂
theorem exists_unique_congr {α : Sort u_1} {p : αProp} {q : αProp} (h : ∀ (a : α), p a q a) :
(∃! a, p a) ∃! a, q a
theorem decide_True' (h : ) :
theorem decide_False' (h : ) :
def Decidable.recOn_true (p : Prop) [h : ] {h₁ : pSort u} {h₂ : ¬pSort u} (h₃ : p) (h₄ : h₁ h₃) :
Decidable.recOn h h₂ h₁
Instances For
def Decidable.recOn_false (p : Prop) [h : ] {h₁ : pSort u} {h₂ : ¬pSort u} (h₃ : ¬p) (h₄ : h₂ h₃) :
Decidable.recOn h h₂ h₁
Instances For
def Decidable.by_cases {p : Prop} {q : Sort u} [dec : ] (h1 : pq) (h2 : ¬pq) :
q

Alias of Decidable.byCases.

Synonym for dite (dependent if-then-else). We can construct an element q (of any sort, not just a proposition) by cases on whether p is true or false, provided p is decidable.

Instances For
theorem Decidable.by_contradiction {p : Prop} [dec : ] (h : ¬pFalse) :
p

Alias of Decidable.byContradiction.

theorem Decidable.not_not_iff {p : Prop} [] :

Alias of Decidable.not_not.

@[deprecated not_or]
theorem Decidable.not_or_iff_and_not (p : Prop) (q : Prop) [] [] :
¬(p q) ¬p ¬q
def Or.decidable {p : Prop} {q : Prop} [dp : ] [dq : ] :

Alias of instDecidableOr.

Instances For
def And.decidable {p : Prop} {q : Prop} [dp : ] [dq : ] :

Alias of instDecidableAnd.

Instances For
def Not.decidable {p : Prop} [dp : ] :

Alias of instDecidableNot.

Instances For
def Iff.decidable {p : Prop} {q : Prop} [] [] :

Alias of instDecidableIff.

Instances For

Alias of instDecidableTrue.

Instances For

Alias of instDecidableFalse.

Instances For
instance instDecidableXor' (p : Prop) {q : Prop} [] [] :
def IsDecEq {α : Sort u} (p : ααBool) :
Instances For
def IsDecRefl {α : Sort u} (p : ααBool) :
Instances For
def decidableEq_of_bool_pred {α : Sort u} {p : ααBool} (h₁ : ) (h₂ : ) :
Instances For
theorem decidableEq_inl_refl {α : Sort u} [h : ] (a : α) :
h a a = isTrue (_ : a = a)
theorem decidableEq_inr_neg {α : Sort u} [h : ] {a : α} {b : α} (n : a b) :
h a b =
theorem rec_subsingleton {p : Prop} [h : ] {h₁ : pSort u} {h₂ : ¬pSort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :
@[deprecated ite_self]
theorem if_t_t (c : Prop) [] {α : Sort u} (t : α) :
(if c then t else t) = t
theorem imp_of_if_pos {c : Prop} {t : Prop} {e : Prop} [] (h : if c then t else e) (hc : c) :
t
theorem imp_of_if_neg {c : Prop} {t : Prop} {e : Prop} [] (h : if c then t else e) (hnc : ¬c) :
e
theorem if_ctx_congr {α : Sort u} {b : Prop} {c : Prop} [dec_b : ] [dec_c : ] {x : α} {y : α} {u : α} {v : α} (h_c : b c) (h_t : cx = u) (h_e : ¬cy = v) :
(if b then x else y) = if c then u else v
theorem if_congr {α : Sort u} {b : Prop} {c : Prop} [] [] {x : α} {y : α} {u : α} {v : α} (h_c : b c) (h_t : x = u) (h_e : y = v) :
(if b then x else y) = if c then u else v
theorem if_ctx_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [dec_b : ] [dec_c : ] (h_c : b c) (h_t : c → (x u)) (h_e : ¬c → (y v)) :
(if b then x else y) if c then u else v
theorem if_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [] [] (h_c : b c) (h_t : x u) (h_e : y v) :
(if b then x else y) if c then u else v
theorem if_ctx_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [] (h_c : b c) (h_t : c → (x u)) (h_e : ¬c → (y v)) :
(if b then x else y) if c then u else v
theorem if_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [] (h_c : b c) (h_t : x u) (h_e : y v) :
(if b then x else y) if c then u else v
theorem dif_ctx_congr {α : Sort u} {b : Prop} {c : Prop} [dec_b : ] [dec_c : ] {x : bα} {u : cα} {y : ¬bα} {v : ¬cα} (h_c : b c) (h_t : ∀ (h : c), x (Iff.mpr h_c h) = u h) (h_e : ∀ (h : ¬c), y (_ : ¬b) = v h) :
dite b x y = dite c u v
theorem dif_ctx_simp_congr {α : Sort u} {b : Prop} {c : Prop} [] {x : bα} {u : cα} {y : ¬bα} {v : ¬cα} (h_c : b c) (h_t : ∀ (h : c), x (Iff.mpr h_c h) = u h) (h_e : ∀ (h : ¬c), y (_ : ¬b) = v h) :
dite b x y = dite c u v
def AsTrue (c : Prop) [] :
Instances For
def AsFalse (c : Prop) [] :
Instances For
theorem AsTrue.get {c : Prop} [h₁ : ] :
c
theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (b : αβ) (h : a₁ = a₂) :
(let x := a₁; b x) = let x := a₂; b x
theorem let_value_heq {α : Sort v} {β : αSort u} {a₁ : α} {a₂ : α} (b : (x : α) → β x) (h : a₁ = a₂) :
HEq (let x := a₁; b x) (let x := a₂; b x)
theorem let_body_eq {α : Sort v} {β : αSort u} (a : α) {b₁ : (x : α) → β x} {b₂ : (x : α) → β x} (h : ∀ (x : α), b₁ x = b₂ x) :
(let x := a; b₁ x) = let x := a; b₂ x
theorem let_eq {α : Sort v} {β : Sort u} {a₁ : α} {a₂ : α} {b₁ : αβ} {b₂ : αβ} (h₁ : a₁ = a₂) (h₂ : ∀ (x : α), b₁ x = b₂ x) :
(let x := a₁; b₁ x) = let x := a₂; b₂ x
def Reflexive {β : Sort v} (r : ββProp) :

A reflexive relation relates every element to itself.

Instances For
def Symmetric {β : Sort v} (r : ββProp) :

A relation is symmetric if x ≺ y implies y ≺ x.

Instances For
def Transitive {β : Sort v} (r : ββProp) :

A relation is transitive if x ≺ y and y ≺ z together imply x ≺ z.

Instances For
theorem Equivalence.reflexive {β : Sort v} {r : ββProp} (h : ) :
theorem Equivalence.symmetric {β : Sort v} {r : ββProp} (h : ) :
theorem Equivalence.transitive {β : Sort v} {r : ββProp} (h : ) :
def Total {β : Sort v} (r : ββProp) :

A relation is total if for all x and y, either x ≺ y or y ≺ x.

Instances For
def Irreflexive {β : Sort v} (r : ββProp) :

Irreflexive means "not reflexive".

Instances For
def AntiSymmetric {β : Sort v} (r : ββProp) :

A relation is antisymmetric if x ≺ y and y ≺ x together imply that x = y.

Instances For
def EmptyRelation {α : Sort u} :
ααProp

An empty relation does not relate any elements.

Instances For
theorem InvImage.trans {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : ) :
theorem InvImage.irreflexive {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : ) :
def Commutative {α : Type u} (f : ααα) :
Instances For
def Associative {α : Type u} (f : ααα) :
Instances For
def LeftIdentity {α : Type u} (f : ααα) (one : α) :
Instances For
def RightIdentity {α : Type u} (f : ααα) (one : α) :
Instances For
def RightInverse {α : Type u} (f : ααα) (inv : αα) (one : α) :
Instances For
def LeftCancelative {α : Type u} (f : ααα) :
Instances For
def RightCancelative {α : Type u} (f : ααα) :
Instances For
def LeftDistributive {α : Type u} (f : ααα) (g : ααα) :
Instances For
def RightDistributive {α : Type u} (f : ααα) (g : ααα) :
Instances For
def RightCommutative {α : Type u} {β : Type v} (h : βαβ) :
Instances For
def LeftCommutative {α : Type u} {β : Type v} (h : αββ) :
Instances For
theorem left_comm {α : Type u} (f : ααα) :
theorem right_comm {α : Type u} (f : ααα) :