mathlib documentation

core.init.logic

@[simp]
theorem opt_param_eq (α : Sort u) (default : α) :
:= default) = α

def id {α : Sort u} :
α → α

Equations
def flip {α : Sort u} {β : Sort v} {φ : Sort w} :
(α → β → φ)β → α → φ

Equations
  • flip f = λ (b : β) (a : α), f a b
def implies  :
Prop → Prop → Prop

Equations
theorem implies.trans {p q r : Prop} :
implies p qimplies q rimplies p r

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

def trivial  :

def absurd {a : Prop} {b : Sort v} :
a → ¬a → b

We can't have a and ¬a, that would be absurd!

Equations
theorem not.intro {a : Prop} :
(a → false)¬a

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

Modus tollens. If an implication is true, then so is its contrapositive.

theorem not_false  :

def non_contradictory  :
Prop → Prop

Equations
theorem non_contradictory_intro {a : Prop} :
a → ¬¬a

def false.elim {C : Sort u} :
false → C

Equations
theorem proof_irrel {a : Prop} (h₁ h₂ : a) :
h₁ = h₂

@[simp]
theorem id.def {α : Sort u} (a : α) :
id a = a

def eq.mp {α β : Sort u} :
α = βα → β

Equations
def eq.mpr {α β : Sort u} :
α = ββ → α

Equations
  • eq.mpr = λ (h₁ : α = β) (h₂ : β), _.rec_on h₂
theorem eq.substr {α : Sort u} {p : α → Prop} {a b : α} :
b = ap ap b

theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} :
f₁ = f₂a₁ = a₂f₁ a₁ = f₂ a₂

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

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

theorem trans_rel_left {α : Sort u} {a b c : α} (r : α → α → Prop) :
r a bb = cr a c

theorem trans_rel_right {α : Sort u} {a b c : α} (r : α → α → Prop) :
a = br b cr a c

theorem of_eq_true {p : Prop} :
p = true → p

theorem not_of_eq_false {p : Prop} :
p = false¬p

def cast {α β : Sort u} :
α = βα → β

Equations
theorem cast_proof_irrel {α β : Sort u} (h₁ h₂ : α = β) (a : α) :
cast h₁ a = cast h₂ a

@[simp]
theorem cast_eq {α : Sort u} (h : α = α) (a : α) :
cast h a = a

def ne {α : Sort u} :
α → α → Prop

Equations
@[simp]
theorem ne.def {α : Sort u} (a b : α) :
a b = ¬a = b

theorem ne.intro {α : Sort u} {a b : α} :
(a = bfalse)a b

theorem ne.elim {α : Sort u} {a b : α} :
a ba = bfalse

theorem ne.irrefl {α : Sort u} {a : α} :
a afalse

theorem ne.symm {α : Sort u} {a b : α} :
a bb a

theorem false_of_ne {α : Sort u} {a : α} :
a afalse

theorem ne_false_of_self {p : Prop} :
p → p false

theorem ne_true_of_not {p : Prop} :
¬p → p true

theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} :
a == bp ap b

theorem heq.subst {α β : Sort u} {a : α} {b : β} {p : Π (T : Sort u), T → Prop} :
a == bp α ap β b

theorem heq.symm {α β : Sort u} {a : α} {b : β} :
a == bb == a

theorem heq_of_eq {α : Sort u} {a a' : α} :
a = a'a == a'

theorem heq.trans {α β φ : Sort u} {a : α} {b : β} {c : φ} :
a == bb == ca == c

theorem heq_of_heq_of_eq {α β : Sort u} {a : α} {b b' : β} :
a == bb = b'a == b'

theorem heq_of_eq_of_heq {α β : Sort u} {a a' : α} {b : β} :
a = a'a' == ba == b

def type_eq_of_heq {α β : Sort u} {a : α} {b : β} :
a == bα = β

theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a) :
h.rec_on p == p

theorem heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') :
e.rec_on p₁ = p₂p₁ == p₂

theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) :
p₁ = e.rec_on p₂p₁ == p₂

theorem of_heq_true {a : Prop} :
a == true → a

theorem eq_rec_compose {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α) :
p₁.rec_on (p₂.rec_on a) = _.rec_on a

theorem cast_heq {α β : Sort u} (h : α = β) (a : α) :
cast h a == a

theorem and.elim {a b c : Prop} :
a b(a → b → c) → c

theorem and.swap {a b : Prop} :
a bb a

def and.symm {a b : Prop} :
a bb a

theorem or.elim {a b c : Prop} :
a b(a → c)(b → c) → c

theorem non_contradictory_em (a : Prop) :
¬¬(a ¬a)

def not_not_em (a : Prop) :
¬¬(a ¬a)

theorem or.swap {a b : Prop} :
a bb a

def or.symm {a b : Prop} :
a bb a

def xor  :
Prop → Prop → Prop

Equations
structure iff  :
Prop → Prop → Prop
  • mp : a → b
  • mpr : b → a

iff P Q, with notation P ↔ Q, is the proposition asserting that P and Q are equivalent, that is, have the same truth value.

theorem iff.elim {a b c : Prop} :
((a → b)(b → a) → c)(a b) → c

theorem iff.elim_left {a b : Prop} :
(a b)a → b

theorem iff.elim_right {a b : Prop} :
(a b)b → a

theorem iff_iff_implies_and_implies (a b : Prop) :
a b (a → b) (b → a)

theorem iff.refl (a : Prop) :
a a

theorem iff.rfl {a : Prop} :
a a

theorem iff.trans {a b c : Prop} :
(a b)(b c)(a c)

theorem iff.symm {a b : Prop} :
(a b)(b a)

theorem iff.comm {a b : Prop} :
a b (b a)

theorem eq.to_iff {a b : Prop} :
a = b(a b)

theorem neq_of_not_iff {a b : Prop} :
¬(a b)a b

theorem not_iff_not_of_iff {a b : Prop} :
(a b)(¬a ¬b)

theorem of_iff_true {a : Prop} :
(a true) → a

theorem not_of_iff_false {a : Prop} :
(a false)¬a

theorem iff_true_intro {a : Prop} :
a → (a true)

theorem iff_false_intro {a : Prop} :
¬a → (a false)

def not_not_not_iff (a : Prop) :

theorem imp_congr {a b c d : Prop} :
(a c)(b d)(a → b c → d)

theorem imp_congr_ctx {a b c d : Prop} :
(a c)(c → (b d))(a → b c → d)

theorem imp_congr_right {a b c : Prop} :
(a → (b c))(a → b a → c)

theorem not_not_intro {a : Prop} :
a → ¬¬a

theorem not_of_not_not_not {a : Prop} :
¬¬¬a → ¬a

@[simp]
theorem not_true  :

@[simp]

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

@[simp]
theorem ne_self_iff_false {α : Sort u} (a : α) :

@[simp]
theorem eq_self_iff_true {α : Sort u} (a : α) :
a = a true

@[simp]
theorem heq_self_iff_true {α : Sort u} (a : α) :
a == a true

@[simp]
theorem iff_not_self (a : Prop) :

@[simp]
theorem not_iff_self (a : Prop) :

@[simp]

@[simp]

theorem eq_comm {α : Sort u} {a b : α} :
a = b b = a

theorem and.imp {a b c d : Prop} :
(a → c)(b → d)a bc d

def and_implies {a b c d : Prop} :
(a → c)(b → d)a bc d

theorem and_congr {a b c d : Prop} :
(a c)(b d)(a b c d)

theorem and_congr_right {a b c : Prop} :
(a → (b c))(a b a c)

theorem and.comm {a b : Prop} :
a b b a

theorem and_comm (a b : Prop) :
a b b a

theorem and.assoc {a b c : Prop} :
(a b) c a b c

theorem and_assoc {c : Prop} (a b : Prop) :
(a b) c a b c

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

theorem and_iff_left {a b : Prop} :
b → (a b a)

theorem and_iff_right {a b : Prop} :
a → (a b b)

@[simp]
theorem and_true (a : Prop) :

@[simp]
theorem true_and (a : Prop) :

@[simp]
theorem and_false (a : Prop) :

@[simp]
theorem false_and (a : Prop) :

@[simp]
theorem not_and_self (a : Prop) :

@[simp]
theorem and_not_self (a : Prop) :

@[simp]
theorem and_self (a : Prop) :
a a a

theorem or.imp {a b c d : Prop} :
(a → c)(b → d)a bc d

theorem or.imp_left {a b c : Prop} :
(a → b)a cb c

theorem or.imp_right {a b c : Prop} :
(a → b)c ac b

theorem or_congr {a b c d : Prop} :
(a c)(b d)(a b c d)

theorem or.comm {a b : Prop} :
a b b a

theorem or_comm (a b : Prop) :
a b b a

theorem or.assoc {a b c : Prop} :
(a b) c a b c

theorem or_assoc {c : Prop} (a b : Prop) :
(a b) c a b c

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

theorem or_iff_right_of_imp {a b : Prop} :
(a → b)(a b b)

theorem or_iff_left_of_imp {a b : Prop} :
(b → a)(a b a)

@[simp]
theorem or_true (a : Prop) :

@[simp]
theorem true_or (a : Prop) :

@[simp]
theorem or_false (a : Prop) :

@[simp]
theorem false_or (a : Prop) :

@[simp]
theorem or_self (a : Prop) :
a a a

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

def or.resolve_left {a b : Prop} :
a b¬a → b

def or.neg_resolve_left {a b : Prop} :
¬a ba → b

def or.resolve_right {a b : Prop} :
a b¬b → a

def or.neg_resolve_right {a b : Prop} :
a ¬bb → a

@[simp]
theorem iff_true (a : Prop) :

@[simp]
theorem true_iff (a : Prop) :

@[simp]
theorem iff_false (a : Prop) :

@[simp]
theorem false_iff (a : Prop) :

@[simp]
theorem iff_self (a : Prop) :

theorem iff_congr {a b c d : Prop} :
(a c)(b d)(a b (c d))

@[simp]
theorem implies_true_iff (α : Sort u) :
α → true true

@[simp]
theorem false_implies_iff (a : Prop) :
false → a true

@[simp]
theorem true_implies_iff (α : Prop) :
true → α α

inductive Exists {α : Sort u} :
(α → Prop) → Prop
  • intro : ∀ {α : Sort u} (p : α → Prop) (w : α), p wExists p

The existential quantifier.

To prove a goal of the form ⊢ ∃ x, p x, you can provide a witness y with the tactic existsi y. If you are working in a project that depends on mathlib, then we recommend the use tactic instead. You'll then be left with the goal ⊢ p y.

To extract a witness x and proof hx : p x from a hypothesis h : ∃ x, p x, use the tactic cases h with x hx. See also the mathlib tactics obtain and rcases.

def exists.intro {α : Sort u_1} {p : α → Prop} (w : α) :
p wExists p

theorem exists.elim {α : Sort u} {p : α → Prop} {b : Prop} :
(∃ (x : α), p x)(∀ (a : α), p a → b) → b

def exists_unique {α : Sort u} :
(α → Prop) → Prop

Equations
theorem exists_unique.intro {α : Sort u} {p : α → Prop} (w : α) :
p w(∀ (y : α), p yy = w)(∃! (x : α), p x)

theorem exists_unique.elim {α : Sort u} {p : α → Prop} {b : Prop} :
(∃! (x : α), p x)(∀ (x : α), p x(∀ (y : α), p yy = x) → b) → b

theorem exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop} :
(∃ (x : α), p x)(∀ (y₁ y₂ : α), p y₁p y₂y₁ = y₂)(∃! (x : α), p x)

theorem exists_of_exists_unique {α : Sort u} {p : α → Prop} :
(∃! (x : α), p x)(∃ (x : α), p x)

theorem unique_of_exists_unique {α : Sort u} {p : α → Prop} (h : ∃! (x : α), p x) {y₁ y₂ : α} :
p y₁p y₂y₁ = y₂

theorem forall_congr {α : Sort u} {p q : α → Prop} :
(∀ (a : α), p a q a)((∀ (a : α), p a) ∀ (a : α), q a)

theorem exists_imp_exists {α : Sort u} {p q : α → Prop} :
(∀ (a : α), p aq a)(∃ (a : α), p a)(∃ (a : α), q a)

theorem exists_congr {α : Sort u} {p q : α → Prop} :
(∀ (a : α), p a q a)(Exists p ∃ (a : α), q a)

theorem exists_unique_congr {α : Sort u} {p₁ p₂ : α → Prop} :
(∀ (x : α), p₁ x p₂ x)(exists_unique p₁ ∃! (x : α), p₂ x)

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

def decidable.to_bool (p : Prop) [h : decidable p] :

Equations
@[simp]

def dite (c : Prop) [h : decidable c] {α : Sort u} :
(c → α)(¬c → α) → α

Equations
  • dite c = λ (t : c → α) (e : ¬c → α), h.rec_on e t
def ite (c : Prop) [h : decidable c] {α : Sort u} :
α → α → α

Equations
  • ite c t e = h.rec_on (λ (hnc : ¬c), e) (λ (hc : c), t)
def decidable.rec_on_true {p : Prop} [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) :
h₁ h₃h.rec_on h₂ h₁

Equations
def decidable.rec_on_false {p : Prop} [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) :
h₂ h₃h.rec_on h₂ h₁

Equations
def decidable.by_cases {p : Prop} {q : Sort u} [φ : decidable p] :
(p → q)(¬p → q) → q

Equations
theorem decidable.em (p : Prop) [decidable p] :
p ¬p

Law of Excluded Middle.

theorem decidable.by_contradiction {p : Prop} [decidable p] :
(¬p → false) → p

theorem decidable.of_not_not {p : Prop} [decidable p] :
¬¬p → p

theorem decidable.not_not_iff (p : Prop) [decidable p] :

theorem decidable.not_and_iff_or_not (p q : Prop) [d₁ : decidable p] [d₂ : decidable q] :
¬(p q) ¬p ¬q

theorem decidable.not_or_iff_and_not (p q : Prop) [d₁ : decidable p] [d₂ : decidable q] :
¬(p q) ¬p ¬q

def decidable_of_decidable_of_iff {p q : Prop} :
decidable p(p q)decidable q

Equations
def or.by_cases {p q : Prop} [decidable p] [decidable q] {α : Sort u} :
p q(p → α)(q → α) → α

Equations
  • h.by_cases h₁ h₂ = dite p (λ (hp : p), h₁ hp) (λ (hp : ¬p), dite q (λ (hq : q), h₂ hq) (λ (hq : ¬q), false.rec α _))
@[instance]
def and.decidable {p q : Prop} [decidable p] [decidable q] :

Equations
@[instance]
def or.decidable {p q : Prop} [decidable p] [decidable q] :

Equations
@[instance]
def not.decidable {p : Prop} [decidable p] :

Equations
@[instance]
def implies.decidable {p q : Prop} [decidable p] [decidable q] :
decidable (p → q)

Equations
@[instance]
def iff.decidable {p q : Prop} [decidable p] [decidable q] :

Equations
@[instance]
def xor.decidable {p q : Prop} [decidable p] [decidable q] :

Equations
@[instance]
def exists_prop_decidable {p : Prop} (P : p → Prop) [Dp : decidable p] [DP : Π (h : p), decidable (P h)] :
decidable (∃ (h : p), P h)

Equations
@[instance]
def forall_prop_decidable {p : Prop} (P : p → Prop) [Dp : decidable p] [DP : Π (h : p), decidable (P h)] :
decidable (∀ (h : p), P h)

Equations
@[instance]
def ne.decidable {α : Sort u} [decidable_eq α] (a b : α) :

Equations
theorem bool.ff_ne_tt  :
ff = ttfalse

def is_dec_eq {α : Sort u} :
(α → α → bool) → Prop

Equations
def is_dec_refl {α : Sort u} :
(α → α → bool) → Prop

Equations
def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} :

Equations
theorem decidable_eq_inl_refl {α : Sort u} [h : decidable_eq α] (a : α) :
h a a = is_true _

theorem decidable_eq_inr_neg {α : Sort u} [h : decidable_eq α] {a b : α} (n : a b) :
h a b = is_false n

@[class]
structure inhabited  :
Sort uSort (max 1 u)
  • default : α

Instances
def arbitrary (α : Sort u) [inhabited α] :
α

Equations
@[instance]
def prop.inhabited  :

Equations
@[instance]
def pi.inhabited (α : Sort u) {β : α → Sort v} [Π (x : α), inhabited (β x)] :
inhabited (Π (x : α), β x)

Equations
@[instance]

Equations
@[instance]

Equations
def nonempty.elim {α : Sort u} {p : Prop} :
nonempty α(α → p) → p

@[simp, instance]
def nonempty_of_inhabited {α : Sort u} [inhabited α] :

theorem nonempty_of_exists {α : Sort u} {p : α → Prop} :
(∃ (x : α), p x)nonempty α

@[class]
inductive subsingleton  :
Sort u → Prop
  • intro : ∀ (α : Sort u), (∀ (a b : α), a = b)subsingleton α

Instances
def subsingleton.elim {α : Sort u} [h : subsingleton α] (a b : α) :
a = b

def subsingleton.helim {α β : Sort u} [h : subsingleton α] (h_1 : α = β) (a : α) (b : β) :
a == b

@[instance]
def subsingleton_prop (p : Prop) :

@[instance]

theorem rec_subsingleton {p : Prop} [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), subsingleton (h₂ h)] :
subsingleton (h.rec_on h₂ h₁)

theorem if_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t e : α} :
ite c t e = t

theorem if_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Sort u} {t e : α} :
ite c t e = e

@[simp]
theorem if_t_t (c : Prop) [h : decidable c] {α : Sort u} (t : α) :
ite c t t = t

theorem implies_of_if_pos {c t e : Prop} [decidable c] :
ite c t ec → t

theorem implies_of_if_neg {c t e : Prop} [decidable c] :
ite c t e¬c → e

theorem if_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} :
(b c)(c → x = u)(¬c → y = v)ite b x y = ite c u v

theorem if_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} :
(b c)x = uy = vite b x y = ite c u v

@[simp]
theorem if_true {α : Sort u} {h : decidable true} (t e : α) :
ite true t e = t

@[simp]
theorem if_false {α : Sort u} {h : decidable false} (t e : α) :
ite false t e = e

theorem if_ctx_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] :
(b c)(c → (x u))(¬c → (y v))(ite b x y ite c u v)

theorem if_congr_prop {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c] :
(b c)(x u)(y v)(ite b x y ite c u v)

theorem if_ctx_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b] (h_c : b c) :
(c → (x u))(¬c → (y v))(ite b x y ite c u v)

theorem if_simp_congr_prop {b c x y u v : Prop} [dec_b : decidable b] (h_c : b c) :
(x u)(y v)(ite b x y ite c u v)

@[simp]
theorem dif_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :
dite c t e = t hc

@[simp]
theorem dif_neg {c : Prop} [h : decidable c] (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :
dite c t e = e hnc

theorem dif_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b c) :
(∀ (h : c), x _ = u h)(∀ (h : ¬c), y _ = v h)dite b x y = dite c u v

theorem dif_ctx_simp_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α} (h_c : b c) :
(∀ (h : c), x _ = u h)(∀ (h : ¬c), y _ = v h)dite b x y = dite c u v

theorem dif_eq_if (c : Prop) [h : decidable c] {α : Sort u} (t e : α) :
dite c (λ (h : c), t) (λ (h : ¬c), e) = ite c t e

@[instance]
def ite.decidable {c t e : Prop} [d_c : decidable c] [d_t : decidable t] [d_e : decidable e] :
decidable (ite c t e)

Equations
@[instance]
def dite.decidable {c : Prop} {t : c → Prop} {e : ¬c → Prop} [d_c : decidable c] [d_t : Π (h : c), decidable (t h)] [d_e : Π (h : ¬c), decidable (e h)] :
decidable (dite c (λ (h : c), t h) (λ (h : ¬c), e h))

Equations
def as_true (c : Prop) [decidable c] :
Prop

Equations
def as_false (c : Prop) [decidable c] :
Prop

Equations
def of_as_true {c : Prop} [h₁ : decidable c] :
as_true c → c

@[ext]
structure ulift  :
Type sType (max s r)
  • down : α

Universe lifting operation

theorem ulift.up_down {α : Type u} (b : ulift α) :
{down := b.down} = b

theorem ulift.down_up {α : Type u} (a : α) :
{down := a}.down = a

structure plift  :
Sort uType u
  • down : α

Universe lifting operation from Sort to Type

theorem plift.up_down {α : Sort u} (b : plift α) :
{down := b.down} = b

theorem plift.down_up {α : Sort u} (a : α) :
{down := a}.down = a

theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) :
a₁ = a₂((let x : α := a₁ in b x) = let x : α := a₂ in b x)

theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π (x : α), β x) :
a₁ = a₂((let x : α := a₁ in b x) == let x : α := a₂ in b x)

theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π (x : α), β x} :
(∀ (x : α), b₁ x = b₂ x)((let x : α := a in b₁ x) = let x : α := a in b₂ x)

theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} :
a₁ = a₂(∀ (x : α), b₁ x = b₂ x)((let x : α := a₁ in b₁ x) = let x : α := a₂ in b₂ x)

def reflexive {β : Sort v} :
(β → β → Prop) → Prop

Equations
def symmetric {β : Sort v} :
(β → β → Prop) → Prop

Equations
  • symmetric r = ∀ ⦃x y : β⦄, r x yr y x
def transitive {β : Sort v} :
(β → β → Prop) → Prop

Equations
  • transitive r = ∀ ⦃x y z : β⦄, r x yr y zr x z
def equivalence {β : Sort v} :
(β → β → Prop) → Prop

Equations
def total {β : Sort v} :
(β → β → Prop) → Prop

Equations
def mk_equivalence {β : Sort v} (r : β → β → Prop) :

def irreflexive {β : Sort v} :
(β → β → Prop) → Prop

Equations
def anti_symmetric {β : Sort v} :
(β → β → Prop) → Prop

Equations
def empty_relation {α : Sort u} :
α → α → Prop

Equations
def subrelation {β : Sort v} :
(β → β → Prop)(β → β → Prop) → Prop

Equations
def inv_image {α : Sort u} {β : Sort v} :
(β → β → Prop)(α → β)α → α → Prop

Equations
  • inv_image r f = λ (a₁ a₂ : α), r (f a₁) (f a₂)
theorem inv_image.trans {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) :

theorem inv_image.irreflexive {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) :

inductive tc {α : Sort u} :
(α → α → Prop)α → α → Prop
  • base : ∀ {α : Sort u} (r : α → α → Prop) (a b : α), r a btc r a b
  • trans : ∀ {α : Sort u} (r : α → α → Prop) (a b c : α), tc r a btc r b ctc r a c

def commutative {α : Type u} :
(α → α → α) → Prop

Equations
def associative {α : Type u} :
(α → α → α) → Prop

Equations
def left_identity {α : Type u} :
(α → α → α)α → Prop

Equations
def right_identity {α : Type u} :
(α → α → α)α → Prop

Equations
def right_inverse {α : Type u} :
(α → α → α)(α → α)α → Prop

Equations
def left_cancelative {α : Type u} :
(α → α → α) → Prop

Equations
def right_cancelative {α : Type u} :
(α → α → α) → Prop

Equations
def left_distributive {α : Type u} :
(α → α → α)(α → α → α) → Prop

Equations
def right_distributive {α : Type u} :
(α → α → α)(α → α → α) → Prop

Equations
def right_commutative {α : Type u} {β : Type v} :
(β → α → β) → Prop

Equations
def left_commutative {α : Type u} {β : Type v} :
(α → β → β) → Prop

Equations
  • left_commutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)
theorem left_comm {α : Type u} (f : α → α → α) :

theorem right_comm {α : Type u} (f : α → α → α) :