ink

def Implies (a : Prop) (b : Prop) : Prop

Equations

• Implies a b = (a → b)

ink

theorem Implies.trans {p : Prop} {q : Prop} {r : Prop} (h₁ : p → q) (h₂ : q → r) : p → r

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

ink

def NonContradictory (a : Prop) : Prop

Equations

• NonContradictory a = ¬¬a

ink

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

Alias of proofIrrel.

ink

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

Alias of congrFun.

ink

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

Alias of congrArg.

ink

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

ink

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

ink

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

ink

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

ink

theorem Ne.def {α : Sort u} (a : α) (b : α) : (a ≠ b) = ¬a = b

ink

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.

ink

theorem heq_of_eq_rec_left {α : Sort u_1} {φ : α → Sort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : e ▸ p₁ = p₂) : HEq p₁ p₂

ink

theorem heq_of_eq_rec_right {α : Sort u_1} {φ : α → Sort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = e ▸ p₂) : HEq p₁ p₂

ink

theorem of_heq_true {a : Prop} (h : HEq a True) : a

ink

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

ink

def Xor' (a : Prop) (b : Prop) : Prop

Equations

• Xor' a b = (a ∧ ¬b ∨ b ∧ ¬a)

ink

instance instTransPropIff : Trans Iff Iff Iff

Equations

• instTransPropIff = { trans := @instTransPropIff.proof_1 }

ink

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

Alias of the forward direction of not_not_not.

ink

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

ink

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

ink

theorem and_true_iff (p : Prop) : p ∧ True ↔ p

ink

theorem true_and_iff (p : Prop) : True ∧ p ↔ p

ink

theorem and_false_iff (p : Prop) : p ∧ False ↔ False

ink

theorem false_and_iff (p : Prop) : False ∧ p ↔ False

ink

theorem and_self_iff (p : Prop) : p ∧ p ↔ p

ink

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

ink

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

ink

theorem true_or_iff (p : Prop) : True ∨ p ↔ True

ink

theorem or_true_iff (p : Prop) : p ∨ True ↔ True

ink

theorem false_or_iff (p : Prop) : False ∨ p ↔ p

ink

theorem or_false_iff (p : Prop) : p ∨ False ↔ p

ink

theorem or_self_iff (p : Prop) : p ∨ p ↔ p

ink

theorem not_or_of_not {a : Prop} {b : Prop} : ¬a → ¬b → ¬(a ∨ b)

ink

theorem iff_true_iff {a : Prop} : (a ↔ True) ↔ a

ink

theorem true_iff_iff {a : Prop} : (True ↔ a) ↔ a

ink

theorem iff_false_iff {a : Prop} : (a ↔ False) ↔ ¬a

ink

theorem false_iff_iff {a : Prop} : (False ↔ a) ↔ ¬a

ink

theorem iff_self_iff (a : Prop) : (a ↔ a) ↔ True

ink

def ExistsUnique {α : Sort u_1} (p : α → Prop) : Prop

Equations

• ExistsUnique p = ∃ x, p x ∧ ∀ (y : α), p y → y = x

ink

def «term∃!_,_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def unexpandExistsUnique : Lean.PrettyPrinter.Unexpander

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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

ink

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

ink

theorem ExistsUnique.exists {α : Sort u_1} {p : α → Prop} : (∃! x, p x) → ∃ x, p x

ink

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

ink

theorem exists_unique_congr {α : Sort u_1} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∃! a, p a) ↔ ∃! a, q a

ink

theorem decide_True' (h : Decidable True) : decide True = true

ink

theorem decide_False' (h : Decidable False) : decide False = false

ink

def Decidable.recOn_true (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_true p h₃ h₄ = cast (_ : h₁ h₃ = Decidable.recOn h h₂ h₁) h₄

ink

def Decidable.recOn_false (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_false p h₃ h₄ = cast (_ : h₂ h₃ = Decidable.recOn h h₂ h₁) h₄

ink

def Decidable.by_cases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q

Alias of Decidable.byCases.

Equations

• @Decidable.by_cases = @Decidable.byCases

ink

theorem Decidable.by_contradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

Alias of Decidable.byContradiction.

ink

theorem Decidable.not_not_iff {p : Prop} [inst : Decidable p] : ¬¬p ↔ p

Alias of Decidable.not_not.

ink

theorem Decidable.not_or_iff_and_not (p : Prop) (q : Prop) [inst : Decidable p] [inst : Decidable q] : ¬(p ∨ q) ↔ ¬p ∧ ¬q

ink

def Or.decidable {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] : Decidable (p ∨ q)

Alias of instDecidableOr.

Equations

• @Or.decidable = @instDecidableOr

ink

def And.decidable {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] : Decidable (p ∧ q)

Alias of instDecidableAnd.

Equations

• @And.decidable = @instDecidableAnd

ink

def Not.decidable {p : Prop} [dp : Decidable p] : Decidable ¬p

Alias of instDecidableNot.

Equations

• @Not.decidable = @instDecidableNot

ink

def Iff.decidable {p : Prop} {q : Prop} [inst : Decidable p] [inst : Decidable q] : Decidable (p ↔ q)

Alias of instDecidableIff.

Equations

• @Iff.decidable = @instDecidableIff

ink

instance instDecidableXor' (p : Prop) {q : Prop} [inst : Decidable p] [inst : Decidable q] : Decidable (Xor' p q)

Equations

• instDecidableXor' p = inferInstanceAs (Decidable (p ∧ ¬q ∨ q ∧ ¬p))

ink

def IsDecEq {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecEq p = ∀ ⦃x y : α⦄, p x y = true → x = y

ink

def IsDecRefl {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecRefl p = ∀ (x : α), p x x = true

ink

def decidableEq_of_bool_pred {α : Sort u} {p : α → α → Bool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) : DecidableEq α

Equations

• decidableEq_of_bool_pred h₁ h₂ x x = match x, x with | x, y => if hp : p x y = true then isTrue (h₁ x y hp) else isFalse (_ : x = y → False)

ink

theorem decidableEq_inl_refl {α : Sort u} [h : DecidableEq α] (a : α) : h a a = isTrue (_ : a = a)

ink

theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a : α} {b : α} (n : a ≠ b) : h a b = isFalse n

ink

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 (Decidable.recOn h h₂ h₁)

ink

theorem if_t_t (c : Prop) [inst : Decidable c] {α : Sort u} (t : α) : (if c then t else t) = t

ink

theorem imp_of_if_pos {c : Prop} {t : Prop} {e : Prop} [inst : Decidable c] (h : if c then t else e) (hc : c) : t

ink

theorem imp_of_if_neg {c : Prop} {t : Prop} {e : Prop} [inst : Decidable c] (h : if c then t else e) (hnc : ¬c) : e

ink

theorem if_ctx_congr {α : Sort u} {b : Prop} {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) : (if b then x else y) = if c then u else v

ink

theorem if_congr {α : Sort u} {b : Prop} {c : Prop} [inst : Decidable b] [inst : Decidable c] {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

ink

theorem if_ctx_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [dec_b : Decidable b] [dec_c : Decidable 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

ink

theorem if_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [inst : Decidable b] [inst : Decidable c] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : (if b then x else y) ↔ if c then u else v

ink

theorem if_ctx_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [inst : Decidable b] (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

ink

theorem if_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [inst : Decidable b] (h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) : (if b then x else y) ↔ if c then u else v

ink

theorem dif_ctx_congr {α : Sort u} {b : Prop} {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 (Iff.mpr h_c h) = u h) (h_e : ∀ (h : ¬c), y (_ : ¬b) = v h) : dite b x y = dite c u v

ink

theorem dif_ctx_simp_congr {α : Sort u} {b : Prop} {c : Prop} [inst : Decidable b] {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

ink

def AsTrue (c : Prop) [inst : Decidable c] : Prop

Equations

• AsTrue c = if c then True else False

ink

def AsFalse (c : Prop) [inst : Decidable c] : Prop

Equations

• AsFalse c = if c then False else True

ink

theorem AsTrue.get {c : Prop} [h₁ : Decidable c] : AsTrue c → c

ink

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

ink

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)

ink

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

ink

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

ink

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

A reflexive relation relates every element to itself.

Equations

• Reflexive r = ((x : β) → r x x)

ink

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

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

Equations

• Symmetric r = (⦃x y : β⦄ → r x y → r y x)

ink

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

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

Equations

• Transitive r = (⦃x y z : β⦄ → r x y → r y z → r x z)

ink

theorem Equivalence.reflexive {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Reflexive r

ink

theorem Equivalence.symmetric {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Symmetric r

ink

theorem Equivalence.transitive {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Transitive r

ink

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

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

Equations

• Total r = ∀ (x y : β), r x y ∨ r y x

ink

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

Irreflexive means "not reflexive".

Equations

• Irreflexive r = ∀ (x : β), ¬r x x

ink

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

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

Equations

• AntiSymmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y

ink

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

An empty relation does not relate any elements.

Equations

• EmptyRelation x x = False

ink

theorem InvImage.trans {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Transitive r) : Transitive (InvImage r f)

ink

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

ink

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

Equations

• Commutative f = ∀ (a b : α), f a b = f b a

ink

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

Equations

• Associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)

ink

def LeftIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• LeftIdentity f one = ∀ (a : α), f one a = a

ink

def RightIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• RightIdentity f one = ∀ (a : α), f a one = a

ink

def RightInverse {α : Type u} (f : α → α → α) (inv : α → α) (one : α) : Prop

Equations

• RightInverse f inv one = ∀ (a : α), f a (inv a) = one

ink

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

Equations

• LeftCancelative f = ∀ (a b c : α), f a b = f a c → b = c

ink

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

Equations

• RightCancelative f = ∀ (a b c : α), f a b = f c b → a = c

ink

def LeftDistributive {α : Type u} (f : α → α → α) (g : α → α → α) : Prop

Equations

• LeftDistributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)

ink

def RightDistributive {α : Type u} (f : α → α → α) (g : α → α → α) : Prop

Equations

• RightDistributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)

ink

def RightCommutative {α : Type u} {β : Type v} (h : β → α → β) : Prop

Equations

• RightCommutative h = ∀ (b : β) (a₁ a₂ : α), h (h b a₁) a₂ = h (h b a₂) a₁

ink

def LeftCommutative {α : Type u} {β : Type v} (h : α → β → β) : Prop

Equations

• LeftCommutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)

ink

theorem left_comm {α : Type u} (f : α → α → α) : Commutative f → Associative f → LeftCommutative f

ink

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

ink

unsafe def WellFounded.fix'.impl {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

Equations

• WellFounded.fix'.impl hwf F x = F x fun y x => WellFounded.fix'.impl hwf F y

ink

@[implemented_by WellFounded.fix'.impl]

def WellFounded.fix' {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

Equations

• WellFounded.fix' hwf F x = WellFounded.fix hwf F x