Аналіз I, Додаток A.7

Вступ до рівності в 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

Варіант цілих чисел, де 12 було примушено дорівнювати 2.

Equations

• NewInt = Quot make_twelve_equal_two

instance instCoeIntNewInt : Coe ℤ NewInt

Приведення цілих чисел до нових цілих чисел

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 ⋯