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

Вступ до рівності в Lean

example : ∑' n:, 9*(10:)^(-(n:)-1) = 1 := ∑' (n : ), 9 * 10 ^ (-n - 1) = 1 ∑' (n : ), 9 * 10 ^ (-n - 1) = ∑' (n : ), 9 / 10 * (1 / 10) ^ n∑' (n : ), 9 / 10 * (1 / 10) ^ n = 1 ∑' (n : ), 9 * 10 ^ (-n - 1) = ∑' (n : ), 9 / 10 * (1 / 10) ^ n (b : ), 9 * 10 ^ (-b - 1) = 9 / 10 * (1 / 10) ^ b n:9 * 10 ^ (-n - 1) = 9 / 10 * (1 / 10) ^ n n:9 * (10 ^ (-n) / 10 ^ 1) = 9 / 10 * (1 / 10 ^ n) n:9 * ((10 ^ n)⁻¹ / 10) = 9 / 10 * (10 ^ n)⁻¹; All goals completed! 🐙 ∑' (n : ), 9 / 10 * (1 / 10) ^ n = 9 / 10 * ∑' (n : ), (1 / 10) ^ n9 / 10 * ∑' (n : ), (1 / 10) ^ n = 1 ∑' (n : ), 9 / 10 * (1 / 10) ^ n = 9 / 10 * ∑' (n : ), (1 / 10) ^ n All goals completed! 🐙 9 / 10 * (1 - 1 / 10)⁻¹ = 1 All goals completed! 🐙example : 12 = (2:Fin 10) := 12 = 2 All goals completed! 🐙

Рефлексивна аксіома

example {X:Type} (x:X) : x = x := X:Typex:Xx = x All goals completed! 🐙
Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a#check Eq.refl
Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a

Аксіома симетрії

example {X:Type} (x y:X) (h: x = y) : y = x := X:Typex:Xy:Xh:x = yy = x All goals completed! 🐙
Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a#check Eq.symm
Eq.symm.{u} {α : Sort u} {a b : α} (h : a = b) : b = a

Аксіома транзитивності

example {X:Type} (x y z:X) (h1: x = y) (h2: y = z) : x = z := X:Typex:Xy:Xz:Xh1:x = yh2:y = zx = z All goals completed! 🐙
Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c#check Eq.trans
Eq.trans.{u} {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c

Аксіома заміщення

example {X Y:Type} (f:X Y) (x y:X) (h: x = y) : f x = f y := X:TypeY:Typef:X Yx:Xy:Xh:x = yf x = f y All goals completed! 🐙
congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂#check congrArg
congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂
def equality_as_equiv_relation (X:Type) : Setoid X := { r a b := a = b iseqv := { refl := Eq.refl symm := Eq.symm trans := Eq.trans } }open Real in /-- Приклад A.7.1 -/ example {x y:} (h:x = y) : 2*x = 2*y sin x = sin y z, x + z = y + z := x:y:h:x = y2 * x = 2 * y sin x = sin y (z : ), x + z = y + z x:y:h:x = y2 * x = 2 * yx:y:h:x = ysin x = sin yx:y:h:x = y (z : ), x + z = y + z x:y:h:x = y2 * x = 2 * y All goals completed! 🐙 x:y:h:x = ysin x = sin y All goals completed! 🐙 x:y:h:x = yz:x + z = y + z All goals completed! 🐙

Приклад A.7.2

example {n m:} (hn: Odd n) (h: n = m) : Odd m := n:m:hn:Odd nh:n = mOdd m n:m:hn:Odd mh:n = mOdd m All goals completed! 🐙
example {n m k:} (hnk: n > k) (h: n = m) : m > k := n:m:k:hnk:n > kh:n = mm > k n:m:k:hnk:m > kh:n = mm > k All goals completed! 🐙open Real in example {x y z:} (hxy : x = sin y) (hyz : y = z^2) : x = sin (z^2) := x:y:z:hxy:x = sin yhyz:y = z ^ 2x = sin (z ^ 2) have : sin y = sin (z^2) := x:y:z:hxy:x = sin yhyz:y = z ^ 2x = sin (z ^ 2) All goals completed! 🐙 All goals completed! 🐙abbrev make_twelve_equal_two : Prop := fun a b a = 12 b = 2

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

abbrev NewInt := Quot make_twelve_equal_two

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

instance : Coe NewInt where coe n := Quot.mk make_twelve_equal_two n
Quot.mk make_twelve_equal_two 2 : Quot make_twelve_equal_two#check ((2:):NewInt)
Quot.mk make_twelve_equal_two 2 : Quot make_twelve_equal_two
Quot.mk make_twelve_equal_two 12 : Quot make_twelve_equal_two#check ((12:):NewInt)
Quot.mk make_twelve_equal_two 12 : Quot make_twelve_equal_two
example : ((12:):NewInt) = ((2:):NewInt) := Quot.mk make_twelve_equal_two 12 = Quot.mk make_twelve_equal_two 2 make_twelve_equal_two 12 2 All goals completed! 🐙theorem NewInt.is_coe (N:NewInt) : n:, N = (n:NewInt) := N:NewInt n, N = Quot.mk make_twelve_equal_two n N:NewInt (a : ), n, Quot.mk make_twelve_equal_two a = Quot.mk make_twelve_equal_two n; N:NewIntn: n_1, Quot.mk make_twelve_equal_two n = Quot.mk make_twelve_equal_two n_1 All goals completed! 🐙abbrev NewInt.quot {X:Type} {f: X} (hf: f 12 = f 2) : NewInt X := X:Typef: Xhf:f 12 = f 2NewInt X X:Typef: Xhf:f 12 = f 2 (a b : ), make_twelve_equal_two a b f a = f b X:Typef: Xhf:f 12 = f 2a:b:make_twelve_equal_two a b f a = f b X:Typef: Xhf:f 12 = f 2a:b:a = 12 b = 2 f a = f b X:Typef: Xhf:f 12 = f 2a:b:ha:a = 12hb:b = 2f a = f b All goals completed! 🐙example {X:Type} {f: X} (hf: f 12 = f 2) (n:) : NewInt.quot hf (n:NewInt) = f n := rfl

Вправа A.7.1

declaration uses 'sorry'example {a b c d:} (hab: a = b) (hcd : c = d) : a + d = b + c := a:b:c:d:hab:a = bhcd:c = da + d = b + c All goals completed! 🐙