Analysis I, Appendix A.7: Equality

Introduction to equality in Lean

def equality_as_equiv_relation (X : Type) : Setoid X

Equations

• equality_as_equiv_relation X = { r := fun (a b : X) => a = b, iseqv := ⋯ }

@[reducible, inline]

abbrev make_twelve_equal_two : ℤ → ℤ → Prop

Equations

• make_twelve_equal_two a b = (a = 12 ∧ b = 2)

@[reducible, inline]

abbrev NewInt : Type

A version of the integers where 12 has been forced to equal 2.

Equations

• NewInt = Quot make_twelve_equal_two

instance instCoeIntNewInt : Coe ℤ NewInt

A coercion from integers to new integers

Equations

• instCoeIntNewInt = { coe := fun (n : ℤ) => Quot.mk make_twelve_equal_two n }

theorem NewInt.is_coe (N : NewInt) : ∃ (n : ℤ), N = Quot.mk make_twelve_equal_two n

@[reducible, inline]

abbrev NewInt.quot {X : Type} {f : ℤ → X} (hf : f 12 = f 2) : NewInt → X

Equations

• NewInt.quot hf = Quot.lift f ⋯