Stream: new members

Topic: clef

Iocta (Jul 21 2020 at 20:29):

What does the name clef mean?

example (u : ℕ → ℝ) (l l' : ℝ) : seq_limit u l → seq_limit u l' → l = l' :=
begin
intros hl hl',
change l ≠ l' at H, -- Lean does not need this line
have ineg : |l-l'| > 0,
exact abs_pos_of_ne_zero (sub_ne_zero_of_ne H),
cases hl ( |l-l'|/4 ) (by linarith) with N hN,
cases hl' ( |l-l'|/4 ) (by linarith) with N' hN',
let N₀ := max N N', -- this is a new tactic, whose effect should be clear
specialize hN N₀ (le_max_left _ _),
specialize hN' N₀ (le_max_right _ _),
have clef : |l-l'| < |l-l'|,
calc
|l - l'| = |(l-u N₀) + (u N₀ -l')|   : by ring
... ≤ |l - u N₀| + |u N₀ - l'|  : by apply abs_add
... = |u N₀ - l| + |u N₀ - l'|  : by rw abs_sub
... < |l-l'|                    : by linarith,
linarith, -- linarith can also find simple numerical contradictions
end


:key:

Iocta (Jul 21 2020 at 20:31):

why is |l-l'| < |l-l'| called that?

Reid Barton (Jul 21 2020 at 20:32):

Because it is the :key: fact.

Iocta (Jul 21 2020 at 20:32):

I see haha

Last updated: Dec 20 2023 at 11:08 UTC