Аналіз 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) ^ n⊢ 9 / 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! 🐙
#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 = y⊢ y = x
All goals completed! 🐙
#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 = z⊢ x = z
All goals completed! 🐙
#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 = y⊢ f x = f y
All goals completed! 🐙
#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 = y⊢ 2 * x = 2 * y ∧ sin x = sin y ∧ ∀ (z : ℝ), x + z = y + z
x:ℝy:ℝh:x = y⊢ 2 * x = 2 * yx:ℝy:ℝh:x = y⊢ sin x = sin yx:ℝy:ℝh:x = y⊢ ∀ (z : ℝ), x + z = y + z
x:ℝy:ℝh:x = y⊢ 2 * x = 2 * y All goals completed! 🐙
x:ℝy:ℝh:x = y⊢ sin 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 = m⊢ Odd m
n:ℤm:ℤhn:Odd mh:n = m⊢ Odd m
All goals completed! 🐙
example {n m k:ℤ} (hnk: n > k) (h: n = m) : m > k := n:ℤm:ℤk:ℤhnk:n > kh:n = m⊢ m > k
n:ℤm:ℤk:ℤhnk:m > kh:n = m⊢ m > 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 ^ 2⊢ x = sin (z ^ 2)
have : sin y = sin (z^2) := x:ℝy:ℝz:ℝhxy:x = sin yhyz:y = z ^ 2⊢ x = 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
#check ((2:ℤ):NewInt)
Quot.mk make_twelve_equal_two 2 : 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 2⊢ NewInt → 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 = 2⊢ f 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
example {a b c d:ℝ} (hab: a = b) (hcd : c = d) : a + d = b + c := a:ℝb:ℝc:ℝd:ℝhab:a = bhcd:c = d⊢ a + d = b + c
All goals completed! 🐙