mathlib docs: core.init.logic

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] :

ite c t e → c → t

source

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

ite c t e → ¬c → e

source

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

source

theorem if_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} :

(b ↔ c) → x = u → 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] :

(b ↔ c) → (c → (x ↔ u)) → (¬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] :

(b ↔ c) → (x ↔ u) → (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) :

(c → (x ↔ u)) → (¬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) :

(x ↔ u) → (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 : c), x _ = u h) → (∀ (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 : c), x _ = u h) → (∀ (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

ite.decidable = ite.decidable._match_1 d_c
ite.decidable._match_1 (decidable.is_true hc) = d_t
ite.decidable._match_1 (decidable.is_false hc) = d_e

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

dite.decidable = dite.decidable._match_1 d_c
dite.decidable._match_1 (decidable.is_true hc) = d_t hc
dite.decidable._match_1 (decidable.is_false hc) = d_e hc

source

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

Prop

Equations

as_true c = ite c true false

source

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

Prop

Equations

as_false c = ite c false true

source

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

as_true c → c

Equations

_ = _
_ = h_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₂ → ((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₂ → ((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} :

(∀ (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₂ → (∀ (x : α), b₁ x = b₂ x) → ((let x : α := a₁ in b₁ x) = let x : α := a₂ in b₂ x)

source

def reflexive {β : Sort v} :

(β → β → Prop) → Prop

Equations

reflexive r = ∀ (x : β), r x x

source

def symmetric {β : Sort v} :

(β → β → Prop) → Prop

Equations

symmetric r = ∀ ⦃x y : β⦄, r x y → r y x

source

def transitive {β : Sort v} :

(β → β → Prop) → Prop

Equations

transitive r = ∀ ⦃x y z : β⦄, r x y → r y z → r x z

source

def equivalence {β : Sort v} :

(β → β → Prop) → Prop

Equations

equivalence r = (reflexive r ∧ symmetric r ∧ transitive r)

source

def total {β : Sort v} :

(β → β → Prop) → Prop

Equations

total r = ∀ (x y : β), r x y ∨ r y x

source

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

reflexive r → symmetric r → transitive r → equivalence r

Equations

_ = _

source

def irreflexive {β : Sort v} :

(β → β → Prop) → Prop

Equations

irreflexive r = ∀ (x : β), ¬r x x

source

def anti_symmetric {β : Sort v} :

(β → β → Prop) → Prop

Equations

anti_symmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y

source

def empty_relation {α : Sort u} :

α → α → Prop

Equations

empty_relation = λ (a₁ a₂ : α), false

source

def subrelation {β : Sort v} :

(β → β → Prop) → (β → β → Prop) → Prop

Equations

subrelation q r = ∀ ⦃x y : β⦄, q x y → r x y

source

def inv_image {α : Sort u} {β : Sort v} :

(β → β → Prop) → (α → β) → α → α → 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 : α → β) :

transitive r → transitive (inv_image r f)

source

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

irreflexive r → irreflexive (inv_image r f)

source

inductive tc {α : Sort u} :

(α → α → Prop) → α → α → 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