mathlib documentation

core.init.logic

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

source
def id {α : Sort u} (a : α) :
α

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

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

Equations
source
theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) :
implies p r

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

source
def trivial  :
true

source
def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) :
b

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

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

source
theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) :
¬a

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

source
theorem not_false  :
¬false

source
def non_contradictory (a : Prop) :
Prop

Equations
source
theorem non_contradictory_intro {a : Prop} (ha : a) :
¬¬a

source
def false.elim {C : Sort u} (h : false) :
C

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

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

source
def eq.mp {α β : Sort u} (a : α = β) (a_1 : α) :
β

Equations
source
def eq.mpr {α β : Sort u} (a : α = β) (a_1 : β) :
α

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

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

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

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

source
theorem trans_rel_left {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : r a b) (h₂ : b = c) :
r a c

source
theorem trans_rel_right {α : Sort u} {a b c : α} (r : α → α → Prop) (h₁ : a = b) (h₂ : r b c) :
r a c

source
theorem of_eq_true {p : Prop} (h : p = true) :
p

source
theorem not_of_eq_false {p : Prop} (h : p = false) :
¬p

source
def cast {α β : Sort u} (h : α = β) (a : α) :
β

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

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

source
def ne {α : Sort u} (a b : α) :
Prop

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

source
theorem ne.intro {α : Sort u} {a b : α} (h : a = b → false) :
a ≠ b

source
theorem ne.elim {α : Sort u} {a b : α} (h : a ≠ b) (a_1 : a = b) :
false

source
theorem ne.irrefl {α : Sort u} {a : α} (h : a ≠ a) :
false

source
theorem ne.symm {α : Sort u} {a b : α} (h : a ≠ b) :
b ≠ a

source
theorem false_of_ne {α : Sort u} {a : α} (a_1 : a ≠ a) :
false

source
theorem ne_false_of_self {p : Prop} (a : p) :
p ≠ false

source
theorem ne_true_of_not {p : Prop} (a : ¬p) :
p ≠ true

source
theorem true_ne_false  :
¬true = false

source
theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a == b) (a_1 : p a) :
p b

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

source
theorem heq.symm {α β : Sort u} {a : α} {b : β} (h : a == b) :
b == a

source
theorem heq_of_eq {α : Sort u} {a a' : α} (h : a = a') :
a == a'

source
theorem heq.trans {α β φ : Sort u} {a : α} {b : β} {c : φ} (h₁ : a == b) (h₂ : b == c) :
a == c

source
theorem heq_of_heq_of_eq {α β : Sort u} {a : α} {b b' : β} (h₁ : a == b) (h₂ : b = b') :
a == b'

source
theorem heq_of_eq_of_heq {α β : Sort u} {a a' : α} {b : β} (h₁ : a = a') (h₂ : a' == b) :
a == b

source
def type_eq_of_heq {α β : Sort u} {a : α} {b : β} (h : a == b) :
α = β

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

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

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

source
theorem of_heq_true {a : Prop} (h : a == true) :
a

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

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

source
theorem and.elim {a b c : Prop} (h₁ : a ∧ b) (h₂ : a → b → c) :
c

source
theorem and.swap {a b : Prop} (a_1 : a ∧ b) :
b ∧ a

source
def and.symm {a b : Prop} (a_1 : a ∧ b) :
b ∧ a

source
theorem or.elim {a b c : Prop} (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → c) :
c

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

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

source
theorem or.swap {a b : Prop} (a_1 : a ∨ b) :
b ∨ a

source
def or.symm {a b : Prop} (a_1 : a ∨ b) :
b ∨ a

source
def xor (a b : Prop) :
Prop

Equations
source
structure iff (a b : 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.

source
theorem iff.elim {a b c : Prop} (a_1 : (a → b) → (b → a) → c) (a_2 : a ↔ b) :
c

source
theorem iff.elim_left {a b : Prop} (a_1 : a ↔ b) (a_2 : a) :
b

source
theorem iff.elim_right {a b : Prop} (a_1 : a ↔ b) (a_2 : b) :
a

source
theorem iff_iff_implies_and_implies (a b : Prop) :
a ↔ b ↔ (a → b) ∧ (b → a)

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

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

source
theorem iff.trans {a b c : Prop} (h₁ : a ↔ b) (h₂ : b ↔ c) :
a ↔ c

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

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

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

source
theorem neq_of_not_iff {a b : Prop} (a_1 : ¬(a ↔ b)) :
a ≠ b

source
theorem not_iff_not_of_iff {a b : Prop} (h₁ : a ↔ b) :
¬a ↔ ¬b

source
theorem of_iff_true {a : Prop} (h : a ↔ true) :
a

source
theorem not_of_iff_false {a : Prop} (a_1 : a ↔ false) :
¬a

source
theorem iff_true_intro {a : Prop} (h : a) :
a ↔ true

source
theorem iff_false_intro {a : Prop} (h : ¬a) :
a ↔ false

source
theorem not_non_contradictory_iff_absurd (a : Prop) :
¬¬¬a ↔ ¬a

source
def not_not_not_iff (a : Prop) :
¬¬¬a ↔ ¬a

source
theorem imp_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a → b ↔ c → d

source
theorem imp_congr_ctx {a b c d : Prop} (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) :
a → b ↔ c → d

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

source
theorem not_not_intro {a : Prop} (ha : a) :
¬¬a

source
theorem not_of_not_not_not {a : Prop} (h : ¬¬¬a) :
¬a

source
@[simp]
theorem not_true  :
¬true ↔ false

source
def not_true_iff  :
¬true ↔ false

source
@[simp]
theorem not_false_iff  :
¬false ↔ true

source
theorem not_congr {a b : Prop} (h : a ↔ b) :
¬a ↔ ¬b

source
@[simp]
theorem ne_self_iff_false {α : Sort u} (a : α) :
¬a = a ↔ false

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

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

source
@[simp]
theorem iff_not_self (a : Prop) :
a ↔ ¬a ↔ false

source
@[simp]
theorem not_iff_self (a : Prop) :
¬a ↔ a ↔ false

source
@[simp]
theorem true_iff_false  :
true ↔ false ↔ false

source
@[simp]
theorem false_iff_true  :
false ↔ true ↔ false

source
theorem false_of_true_iff_false (a : true ↔ false) :
false

source
theorem false_of_true_eq_false (a : true = false) :
false

source
theorem true_eq_false_of_false (a : false) :
true = false

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

source
theorem and.imp {a b c d : Prop} (hac : a → c) (hbd : b → d) (a_1 : a ∧ b) :
c ∧ d

source
def and_implies {a b c d : Prop} (hac : a → c) (hbd : b → d) (a_1 : a ∧ b) :
c ∧ d

source
theorem and_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a ∧ b ↔ c ∧ d

source
theorem and_congr_right {a b c : Prop} (h : a → (b ↔ c)) :
a ∧ b ↔ a ∧ c

source
theorem and.comm {a b : Prop} :
a ∧ b ↔ b ∧ a

source
theorem and_comm (a b : Prop) :
a ∧ b ↔ b ∧ a

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

source
theorem and_assoc {c : Prop} (a b : Prop) :
(a ∧ b) ∧ c ↔ a ∧ b ∧ c

source
theorem and.left_comm {a b c : Prop} :
a ∧ b ∧ c ↔ b ∧ a ∧ c

source
theorem and_iff_left {a b : Prop} (hb : b) :
a ∧ b ↔ a

source
theorem and_iff_right {a b : Prop} (ha : a) :
a ∧ b ↔ b

source
@[simp]
theorem and_true (a : Prop) :
a ∧ true ↔ a

source
@[simp]
theorem true_and (a : Prop) :
true ∧ a ↔ a

source
@[simp]
theorem and_false (a : Prop) :
a ∧ false ↔ false

source
@[simp]
theorem false_and (a : Prop) :
false ∧ a ↔ false

source
@[simp]
theorem not_and_self (a : Prop) :
¬a ∧ a ↔ false

source
@[simp]
theorem and_not_self (a : Prop) :
a ∧ ¬a ↔ false

source
@[simp]
theorem and_self (a : Prop) :
a ∧ a ↔ a

source
theorem or.imp {a b c d : Prop} (h₂ : a → c) (h₃ : b → d) (a_1 : a ∨ b) :
c ∨ d

source
theorem or.imp_left {a b c : Prop} (h : a → b) (a_1 : a ∨ c) :
b ∨ c

source
theorem or.imp_right {a b c : Prop} (h : a → b) (a_1 : c ∨ a) :
c ∨ b

source
theorem or_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a ∨ b ↔ c ∨ d

source
theorem or.comm {a b : Prop} :
a ∨ b ↔ b ∨ a

source
theorem or_comm (a b : Prop) :
a ∨ b ↔ b ∨ a

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

source
theorem or_assoc {c : Prop} (a b : Prop) :
(a ∨ b) ∨ c ↔ a ∨ b ∨ c

source
theorem or.left_comm {a b c : Prop} :
a ∨ b ∨ c ↔ b ∨ a ∨ c

source
theorem or_iff_right_of_imp {a b : Prop} (ha : a → b) :
a ∨ b ↔ b

source
theorem or_iff_left_of_imp {a b : Prop} (hb : b → a) :
a ∨ b ↔ a

source
@[simp]
theorem or_true (a : Prop) :
a ∨ true ↔ true

source
@[simp]
theorem true_or (a : Prop) :
true ∨ a ↔ true

source
@[simp]
theorem or_false (a : Prop) :
a ∨ false ↔ a

source
@[simp]
theorem false_or (a : Prop) :
false ∨ a ↔ a

source
@[simp]
theorem or_self (a : Prop) :
a ∨ a ↔ a

source
theorem not_or {a b : Prop} (a_1 : ¬a) (a_2 : ¬b) :
¬(a ∨ b)

source
def or.resolve_left {a b : Prop} (h : a ∨ b) (na : ¬a) :
b

source
def or.neg_resolve_left {a b : Prop} (h : ¬a ∨ b) (ha : a) :
b

source
def or.resolve_right {a b : Prop} (h : a ∨ b) (nb : ¬b) :
a

source
def or.neg_resolve_right {a b : Prop} (h : a ∨ ¬b) (hb : b) :
a

source
@[simp]
theorem iff_true (a : Prop) :
a ↔ true ↔ a

source
@[simp]
theorem true_iff (a : Prop) :
true ↔ a ↔ a

source
@[simp]
theorem iff_false (a : Prop) :
a ↔ false ↔ ¬a

source
@[simp]
theorem false_iff (a : Prop) :
false ↔ a ↔ ¬a

source
@[simp]
theorem iff_self (a : Prop) :
a ↔ a ↔ true

source
theorem iff_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
a ↔ b ↔ (c ↔ d)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem to_bool_true_eq_tt (h : decidable true) :
to_bool true = tt

source
@[simp]
theorem to_bool_false_eq_ff (h : decidable false) :
to_bool false = ff

source
@[instance]
def decidable.true  :
decidable true

Equations
source
@[instance]
def decidable.false  :
decidable false

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

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

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

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

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

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

Law of Excluded Middle.

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

source
theorem decidable.of_not_not {p : Prop} [decidable p] (a : ¬¬p) :
p

source
theorem decidable.not_not_iff (p : Prop) [decidable p] :
¬¬p ↔ p

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

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

source
def decidable_of_decidable_of_iff {p q : Prop} (hp : decidable p) (h : p ↔ q) :
decidable q

Equations
source
def decidable_of_decidable_of_eq {p q : Prop} (hp : decidable p) (h : p = q) :
decidable q

Equations
source
def or.by_cases {p q : Prop} [decidable p] [decidable q] {α : Sort u} (h : p ∨ q) (h₁ : p → α) (h₂ : 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 α _))
source
@[instance]
def and.decidable {p q : Prop} [decidable p] [decidable q] :
decidable (p ∧ q)

Equations
source
@[instance]
def or.decidable {p q : Prop} [decidable p] [decidable q] :
decidable (p ∨ q)

Equations
source
@[instance]
def not.decidable {p : Prop} [decidable p] :
decidable (¬p)

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

Equations
source
@[instance]
def iff.decidable {p q : Prop} [decidable p] [decidable q] :
decidable (p ↔ q)

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

Equations
source
@[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
source
@[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
source
@[instance]
def ne.decidable {α : Sort u} [decidable_eq α] (a b : α) :
decidable (a ≠ b)

Equations
source
theorem bool.ff_ne_tt (a : ff = tt) :
false

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

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

Equations
source
@[instance]
def bool.decidable_eq  :
decidable_eq bool

Equations
source
def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) :
decidable_eq α

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

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

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

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

Equations
source
@[instance]
def prop.inhabited  :
inhabited Prop

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

Equations
source
@[instance]
def bool.inhabited  :
inhabited bool

Equations
source
@[instance]
def true.inhabited  :
inhabited true

Equations
source
@[class]
inductive nonempty (α : Sort u) :
Prop
  • intro : ∀ (α : Sort u), α → nonempty α

Instances
source
def nonempty.elim {α : Sort u} {p : Prop} (h₁ : nonempty α) (h₂ : α → p) :
p

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

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

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

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

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

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

source
@[instance]
def decidable.subsingleton (p : Prop) :
subsingleton (decidable p)

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

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

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

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

source
theorem implies_of_if_pos {c t e : Prop} [decidable c] (h : ite c t e) (a : c) :
t

source
theorem implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) (a : ¬c) :
e

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

source
theorem if_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) :
ite b x y = ite c u v

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

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

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

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

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

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

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

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

source
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_t : ∀ (h : c), x _ = u h) (h_e : ∀ (h : ¬c), y _ = v h) :
dite b x y = dite c u v

source
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_t : ∀ (h : c), x _ = u h) (h_e : ∀ (h : ¬c), y _ = v h) :
dite b x y = dite c u v

source
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

source
@[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
source
@[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
source
def as_true (c : Prop) [decidable c] :
Prop

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

Equations
source
def of_as_true {c : Prop} [h₁ : decidable c] (h₂ : as_true c) :
c

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

Universe lifting operation

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

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

source
structure plift (α : Sort u) :
Type u
  • down : α

Universe lifting operation from Sort to Type

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

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

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

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

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

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

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

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

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

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

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

Equations
source
def mk_equivalence {β : Sort v} (r : β → β → Prop) (rfl : reflexive r) (symm : symmetric r) (trans : transitive r) :
equivalence r

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

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

Equations
source
def empty_relation {α : Sort u} (a₁ a₂ : α) :
Prop

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

Equations
source
def inv_image {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (a a_1 : α) :
Prop

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

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

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

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

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

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

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

Equations
source
def right_inverse {α : Type u} (f : α → α → α) (inv : α → α) (one : α) :
Prop

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

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

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

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

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

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

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

source
theorem right_comm {α : Type u} (f : α → α → α) (a : commutative f) (a_1 : associative f) :
right_commutative f