-
Notifications
You must be signed in to change notification settings - Fork 0
/
sample_questions_and_solutions.lean
55 lines (41 loc) · 1.39 KB
/
sample_questions_and_solutions.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
/-
I am a .lean file about the real numbers. You can interact with me online at
TinyURL.com/real-numbers-in-lean
or if you have lean and mathlib installed on your computer,
you can download me from https://github.com/kbuzzard/real-numbers-course
and open me in VS Code on your computer, for a faster experience.
See the currently non-existing documentation at the link above;
until it's written nobody will have a chance of being
able to do anything.
-/
-- Import mathlib's real number module.
import data.real.basic
-- Now we have a version of the real numbers which mathematicians
-- can learn to use. It's sometimes fun and sometimes frustrating
-- to play with. At Zulip we're trying to make it more fun and
-- less frustrating for mathematicians.
import tactic.linarith
-- Now we have some really cool tactics
lemma question1 : (2 : ℝ) + (2 : ℝ) = (4 : ℝ) :=
begin
sorry
end
lemma question2 (x y : ℝ) : x + y = y + x :=
begin
sorry
end
lemma question3 : ∀ x y : ℝ, (x + y) ^ 3 = x ^ 3 + 3 * x ^ 2 + 3 * x + 1 :=
begin
sorry
end
lemma question4 : ∀ (a b c : ℝ), (c ≠ 0) → a / c + b / c = (a + b) / c :=
begin
sorry
end
lemma question5 : ∀ (a b c : ℝ), a / c + b / c = (a + b) / c :=
begin
sorry
end
-- need basic questions about sequences, but I don't know the idiomatic way
-- to talk about limits of sequences in Lean
#check limit.is_limit