It is quite hard to explain without further context, don't you think? I mean when you say something like: For anything X is true, then it means that given any "thing"/object X is true about that thing, right?
@MaxH What you say is fine, but the point is that there is no reason to think that you can make statements about anything other than objects. Everything is an object.
@user21820 I wanted to prove the fraction law , if limit(f) is L , then limit(1/f) = 1/L. I first wanted to use asympatotic analysis for that. But after 1 / (v + o(1)) = 1 / (v + o(1)) + 1/v - 1/v , I don't know how to go further.
@Prithubiswas 1/(1+o(1)) ⊆ 1+o(1). This is usually taken as an axiom in asymptotic analysis. Then given constant v ≠ 0 we would have 1/(v+o(1)) = 1/(v+o(v)) = 1/v · 1/(1+o(1)) ⊆ 1/v · (1+o(1)) = 1/v+o(1).
Alternatively, and more generally, you can take as an axiom 1/(1+x) ∈ 1−x+o(x) for x ≈ 0. Actually you have higher expansions as well, such as 1/(1+x) ∈ 1−x+O(x^2) for x ≈ 0.
From this we get 1/(1+o(1)) ⊆ 1−o(1)+o(o(1)) = 1+o(1). We also get 1/(1+x^3) ∈ 1−x^3+O(x^6) as x → 0.
Asymptotic analysis is basically about using asymptotic expansions as axiomatic, and this can be done rigorously as above. So for this we are actually using the asymptotic expansion for 1/(1+x) for x ≈ 0.
@Prithubiswas As for turning the asymptotic analysis into a proof of the limit theorem, we can apply the same technique as before; we wish to bound the x so as to bound the −x+o(x). One easy way for real analysis is to simply find concrete bounds: 1−x ≤ 1/(1+x) ≤ 1−x+2·x^2 for every x∈ℝ[≥−1/2].
This doesn't work for complex x. For that you would need manipulation of abs.
If you use 1/(1+x) ∈ 1+O(x), then you need abs( 1/(1+x) − 1 ) = abs(x) / abs(1+x) ≤ abs(x) / ( abs(1) − abs(−x) ).
If you use 1/(1+x) ∈ 1−x+O(x^2), then you need abs( 1/(1+x) − (1−x) ) = abs(x^2) / abs(1+x) ≤ abs(x^2) / ( abs(1) − abs(−x) ).
@Prithubiswas: Incidentally, the more general asymptotic expansion can be derived from the 'trivial' 1/(1+o(1)) ⊆ 1+o(1).
For example, for x ≈ 0 we have 1/(1+x) = 1−x+x^2/(1+x) ∈ 1−x+x^2/(1+o(1)) ⊆ 1−x+x^2·(1+o(1)) ⊆ 1−x+O(x^2).
So if you set out to axiomatize asymptotic analysis, you would find that you can get a lot using simple axioms for arithmetic with asymptotic expressions. The ones for addition and subtraction and multiplication are obvious. The above 'trivial' axiom is for division.
@user21820 I think I will try on my own to turn the asymptotic proof into an ε-δ proof.
# ∀x,y ∈ ℝ (abs(x+y) ≤ abs(x) + abs(y)) [triangle inequality]
Given a,b ∈ ℝ
If a ≥ 0 ∧ b ≥ 0 :
a + b ≥ 0
abs(a + b) = a + b = abs(a) + abs(b)
If a < 0 ∧ b < 0 :
a + b < 0
abs(a + b) = -(a + b)
= -a + -b
= abs(a) + abs(b)
abs(a + b) = a + b = abs(a) + abs(b)
If a ≥ 0 ∧ b < 0 :
If a + b ≥ 0 :
abs(a + b) = a + b
< a + -b [b < 0 < -b]
= abs(a) + abs(b)
abs(a + b) < abs(a) + abs(b)
If a + b < 0 :
abs(a + b) = -a + -b
≤ a + -b [-a ≤ 0 ≤ a]
@user21820 attempt #1 at proving the Triangle Inequality for abs(x).
@Prithubiswas Looks good. You can factor out the symmetric proof by first proving ∀x,y∈ℝ ( x < 0 ≤ y ⇒ abs(x+y) ≤ abs(x)+abs(y) ) and then applying it twice to get your last two cases.
@user21820 Of course. In many proofs, I have seen "WLOG" in such cases. What's your preferred way of doing this (in a formal way) ? You have shown me different forms, in the past months. I am wondering what you do when one proof is the same as other only with two variables interchanged.
That seems to be the case here, so it works. After all, your subproof just needs one more line to yield ∀x,y∈ℝ ( y < 0 ≤ x ⇒ abs(x+y) ≤ abs(x)+abs(y) ). So it seems worth it here.
Plot twist 1: It is revealed (in line with your idea) that the antagonist came across ancient records of an ancient seal enacted to seal out a great and terrible power, and saw someone involved that had so many similarities to himself that he concluded he must go back in time otherwise that ancie...
Do you see any plot-hole? (Suppressing disbelief about time-travel fixing futures; I have a way to fix that but it's not relevant to the story.)
Now this still looks ugly, because the underlying system does not have conditional expressions, which are well-known to any programmer but somehow didn't make it into logic texts. "( C ? x : y )" is a well-known programming syntax that means ( x if C but y otherwise ). If we had this, we could simply let min = ( ℝ^2 p ↦ ( first(p) < second(p) ? first(p) : second(p) ) ) and be done with it.
