core / init.core - mathlib docs

An abbreviation for punit.{0}, its most common instantiation. This type should be preferred over punit where possible to avoid unnecessary universe parameters.

source

def unit.star :

unit

source

def thunk (α : Type u) :

Type u

Gadget for defining thunks, thunk parameters have special treatment. Example: given def f (s : string) (t : thunk nat) : nat an application f "hello" 10 is converted into f "hello" (λ _, 10)

source

inductive true :

Prop

intro : true

source

inductive false :

Prop

source

inductive empty :

Type

source

def not (a : Prop) :

Prop

Logical not.

not P, with notation ¬ P, is the Prop which is true if and only if P is false. It is internally represented as P → false, so one way to prove a goal ⊢ ¬ P is to use intro h, which gives you a new hypothesis h : P and the goal ⊢ false.

A hypothesis h : ¬ P can be used in term mode as a function, so if w : P then h w : false.

Related mathlib tactic: contrapose.

source

inductive eq {α : Sort u} (a : α) :

α → Prop

refl : ∀ {α : Sort u} (a : α), a = a

source

inductive heq {α : Sort u} (a : α) {β : Sort u} :

β → Prop

refl : ∀ {α : Sort u} (a : α), a == a

Heterogeneous equality.

Its purpose is to write down equalities between terms whose types are not definitionally equal. For example, given x : vector α n and y : vector α (0+n), x = y doesn't typecheck but x == y does.

If you have a goal ⊢ x == y, your first instinct should be to ask (either yourself, or on zulip) if something has gone wrong already. If you really do need to follow this route, you may find the lemmas eq_rec_heq and eq_mpr_heq useful.

source

structure prod (α : Type u) (β : Type v) :

Type (max u v)

fst : α
snd : β

source

structure pprod (α : Sort u) (β : Sort v) :

Sort (max 1 u v)

fst : α
snd : β

Similar to prod, but α and β can be propositions. We use this type internally to automatically generate the brec_on recursor.

source

structure and (a b : Prop) :

Prop

left : a
right : b

Logical and.

and P Q, with notation P ∧ Q, is the Prop which is true precisely when P and Q are both true.

To prove a goal ⊢ P ∧ Q, you can use the tactic split, which gives two separate goals ⊢ P and ⊢ Q.

Given a hypothesis h : P ∧ Q, you can use the tactic cases h with hP hQ to obtain two new hypotheses hP : P and hQ : Q. See also the obtain or rcases tactics in mathlib.

source

theorem and.elim_left {a b : Prop} (h : a ∧ b) :

a

source

theorem and.elim_right {a b : Prop} (h : a ∧ b) :

b

source

@[nolint]

def rfl {α : Sort u} {a : α} :

a = a

source

theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) :

P b

source

theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) :

a = c

source

theorem eq.symm {α : Sort u} {a b : α} (h : a = b) :

b = a

source

def heq.rfl {α : Sort u} {a : α} :

a == a

source

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

a = a'

source

inductive sum (α : Type u) (β : Type v) :

Type (max u v)

inl : Π {α : Type u} {β : Type v}, α → α ⊕ β
inr : Π {α : Type u} {β : Type v}, β → α ⊕ β

source

inductive psum (α : Sort u) (β : Sort v) :

Sort (max 1 u v)

inl : Π {α : Sort u} {β : Sort v}, α → psum α β
inr : Π {α : Sort u} {β : Sort v}, β → psum α β

source

inductive or (a b : Prop) :

Prop

inl : ∀ {a b : Prop}, a → a ∨ b
inr : ∀ {a b : Prop}, b → a ∨ b

Logical or.

or P Q, with notation P ∨ Q, is the proposition which is true if and only if P or Q is true.

To prove a goal ⊢ P ∨ Q, if you know which alternative you want to prove, you can use the tactics left (which gives the goal ⊢ P) or right (which gives the goal ⊢ Q).

Given a hypothesis h : P ∨ Q and goal ⊢ R, the tactic cases h will give you two copies of the goal ⊢ R, with the hypothesis h : P in the first, and the hypothesis h : Q in the second.

source

theorem or.intro_left {a : Prop} (b : Prop) (ha : a) :

a ∨ b

source

theorem or.intro_right (a : Prop) {b : Prop} (hb : b) :

a ∨ b

source

structure sigma {α : Type u} (β : α → Type v) :

Type (max u v)