Homotopy Type Theory
limit of a binary function approaching a diagonal > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Contents
Definition
Let T T be a function limit space with a tight apartness relation # \# and let S ⊆ T S \subseteq T be a subtype of T T . Let us define the subtype Δ # ( S ) ⊆ S × S \Delta_{\#}(S) \subseteq S \times S of pairs of elements apart from the diagonal as
Δ # ( S ) ≔ ∑ ( x , y ) : S × S x # y \Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y
Given Let apartial U U binary be function a type such that q : Δ # ( S ) → ⊆ T U q:\Delta_{\#}(S) \Delta_{\#}(S) \to \subseteq T U , the and currying of q U ⊆ S × S q U \subseteq S \times S . results As in a the result, dependent for functions every x : S x:S , there is a dependent type
x : S ⊢ q ( x ) : ( ∑ y : S x # y ) → T x:S \vdash q(x): \left(\sum_{y:S} x \# y\right) \to T U ( x ) ≔ ∑ y : S ( x , y ) U(x) \coloneqq \sum_{y:S} (x, y)
A Given function a g : S → T g:S \to T partial is binary a function limit of q q approaching the diagonal q : U → T q:U \to T , if the for currying all of x q : S x:S q results in the limit of the dependent function functions q ( x ) q(x) approaching x x is g ( x ) g(x) . We can define a predicate that the q q has a limit approaching the diagonal as
hasLimitApproachingDiagonal x ( : S ⊢ q ( x ) ≔ : [ ( ∑ g y : S U → ( F x ) ∏ x : S lim y → x q ( x ) , ( y ) = ) g ( x ) ] → T hasLimitApproachingDiagonal(q) x:S \coloneqq \vdash \left[\sum_{g:S q(x): \left(\sum_{y:U(x)} (x,y)\right) \to F} T \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]
The A type function of all functions inΔ # g ( : S ) → F T \Delta_{\#}(S) g:S \to F T that have a limit approaching the diagonal is defined a as limit of q q approaching the diagonal if for all x : S x:S the limit of the dependent function q ( x ) q(x) approaching x x is g ( x ) g(x) . We can define a predicate that the q q has a limit approaching the diagonal as
DiagonalLimitFunc ( S , T ) ≔ ∑ q : Δ # ( S ) → T hasLimitApproachingDiagonal ( q ) ≔ [ ∑ g : S → T ∏ x : S lim y → x q ( x ) ( y ) = g ( x ) ] DiagonalLimitFunc(S, hasLimitApproachingDiagonal(q) T) \coloneqq \sum_{q:\Delta_{\#}(S) \left[\sum_{g:S \to T} hasLimitApproachingDiagonal(q) \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]
The type of all functions in U → T U \to T that have a limit approaching the diagonal is defined as
DiagLimFunc ( S , T ) ≔ ∑ q : U → T hasLimitApproachingDiagonal ( q ) DiagLimFunc(S, T) \coloneqq \sum_{q:U \to T} hasLimitApproachingDiagonal(q)
As a result, there exists a function
lim ( x , y ) → ( x , x ) ( − ) ( x , y ) : DiagonalLimitFunc DiagLimFunc ( S , T ) → ( S → F ) \lim_{(x, y) \to (x, x)} (-)(x, y): DiagonalLimitFunc(S, DiagLimFunc(S, T) \to (S \to F)
which returns the limit of a partial binary function q : DiagonalLimitFunc DiagLimFunc ( S , T ) ⊆ ( Δ # ( S ) → T ) q:DiagonalLimitFunc(S, q:DiagLimFunc(S, T) \subseteq (\Delta_{\#}(S) \to T) approaching the diagonal and thus satisfies the equation algebraic limit theorem s
∏ x : S lim y → x q ( x ) ( y ) = lim ( x , y ) → ( x , x ) q ( x , y ) \prod_{x:S} \lim_{y \to x} q(x)(y) = \lim_{(x, y) \to (x, x)} q(x, y)
Properties
In a calculus field? F F , the algebraic limit theorem s are satisfied:
Limits preserve the zero function
∏ x : S lim ( x , y ) → ( x , x ) 0 ( x , y ) = lim y → x 0 ( x ) ( y ) \prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = \lim_{y \to x} 0(x)(y) ∏ x : S lim ( x , y ) → ( x , x ) 0 ( x , y ) = 0 \prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0 ∏ x : S lim ( x , y ) → ( x , x ) 0 ( x , y ) = 0 ( x , x ) \prod_{x:S} \lim_{(x, y) \to (x, x)} 0(x, y) = 0(x, x)
Limits preserve addition of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) + g ( x , y ) = lim ( x , y ) → ( x , x ) ( f + g ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} (f + g)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) + g ( x , y ) = lim y → x ( f + g ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} (f + g)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) + g ( x , y ) = lim y → x f ( x ) ( y ) + g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) + g ( x , y ) = lim y → x f ( x ) ( y ) + lim y → x g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{y \to x} f(x)(y) + \lim_{y \to x} g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) + g ( x , y ) = lim ( x , y ) → ( x , x ) f ( x , y ) + lim ( x , y ) → ( x , x ) g ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) + g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) + \lim_{(x, y) \to (x, x)} g(x, y)
Limits preserve negation of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) − f ( x , y ) = lim y → x − f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = \lim_{y \to x} -f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) − f ( x , y ) = − lim y → x f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{y \to x} f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) − f ( x , y ) = − lim ( x , y ) → ( x , x ) f ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} -f(x, y) = -\lim_{(x, y) \to (x, x)} f(x, y)
Limits preserve subtraction of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) − g ( x , y ) = lim ( x , y ) → ( x , x ) ( f − g ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} (f - g)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) − g ( x , y ) = lim y → x ( f − g ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} (f - g)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) − g ( x , y ) = lim y → x f ( x ) ( y ) − g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) − g ( x , y ) = lim y → x f ( x ) ( y ) − lim y → x g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{y \to x} f(x)(y) - \lim_{y \to x} g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) − g ( x , y ) = lim ( x , y ) → ( x , x ) f ( x , y ) − lim ( x , y ) → ( x , x ) g ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) - g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) - \lim_{(x, y) \to (x, x)} g(x, y)
Limits preserve the left multiplicative ℤ \mathbb{Z} -action of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℤ lim ( x , y ) → ( x , x ) n f ( x , y ) = lim ( x , y ) → ( x , x ) ( n f ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{(x, y) \to (x, x)} (n f)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℤ lim ( x , y ) → ( x , x ) n f ( x , y ) = lim y → x ( n f ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} (n f)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℤ lim ( x , y ) → ( x , x ) n f ( x , y ) = lim y → x n f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = \lim_{y \to x} n f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℤ lim ( x , y ) → ( x , x ) n f ( x , y ) = n lim y → x f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{y \to x} f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℤ lim ( x , y ) → ( x , x ) n f ( x , y ) = n lim ( x , y ) → ( x , x ) f ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{Z}} \lim_{(x, y) \to (x, x)} n f(x, y) = n \lim_{(x, y) \to (x, x)} f(x, y)
Limits preserve multiplication of functions by scalars
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ a : F lim ( x , y ) → ( x , x ) a f ( x , y ) = lim ( x , y ) → ( x , x ) ( a f ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{(x, y) \to (x, x)} (a f)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ a : F lim ( x , y ) → ( x , x ) a f ( x , y ) = lim y → x ( a f ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} (a f)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ a : f lim ( x , y ) → ( x , x ) a f ( x , y ) = lim y → x a f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:f} \lim_{(x, y) \to (x, x)} a f(x, y) = \lim_{y \to x} a f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ a : F lim ( x , y ) → ( x , x ) a f ( x , y ) = a lim y → x f ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{y \to x} f(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ a : F lim ( x , y ) → ( x , x ) a f ( x , y ) = a lim ( x , y ) → ( x , x ) f ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{a:F} \lim_{(x, y) \to (x, x)} a f(x, y) = a \lim_{(x, y) \to (x, x)} f(x, y)
Limits preserve the one function
∏ x : S lim ( x , y ) → ( x , x ) 1 ( x , y ) = lim y → x 1 ( x ) ( y ) \prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = \lim_{y \to x} 1(x)(y) ∏ x : S lim ( x , y ) → ( x , x ) 1 ( x , y ) = 1 \prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1 ∏ x : S lim ( x , y ) → ( x , x ) 1 ( x , y ) = 1 ( x , x ) \prod_{x:S} \lim_{(x, y) \to (x, x)} 1(x, y) = 1(x, x)
Limits preserve multiplication of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ g ( x , y ) = lim ( x , y ) → ( x , x ) ( f ⋅ g ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} (f \cdot g)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ g ( x , y ) = lim y → x ( f ⋅ g ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} (f \cdot g)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ g ( x , y ) = lim y → x f ( x ) ( y ) ⋅ g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ g ( x , y ) = lim y → x f ( x ) ( y ) ⋅ lim y → x g ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{y \to x} f(x)(y) \cdot \lim_{y \to x} g(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ g : DiagLimFunc ( S , F ) lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ g ( x , y ) = lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ lim ( x , y ) → ( x , x ) g ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{g:DiagLimFunc(S, F)} \lim_{(x, y) \to (x, x)} f(x, y) \cdot g(x, y) = \lim_{(x, y) \to (x, x)} f(x, y) \cdot \lim_{(x, y) \to (x, x)} g(x, y)
Limits preserve powers of functions
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ lim ( x , y ) → ( x , x ) f ( x , y ) n = lim ( x , y ) → ( x , x ) ( f n ) ( x , y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{(x, y) \to (x, x)} (f^n)(x, y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ lim ( x , y ) → ( x , x ) f ( x , y ) n = lim y → x ( f n ) ( x ) ( y ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f^n)(x)(y) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ lim ( x , y ) → ( x , x ) f ( x , y ) n = lim y → x ( f ( x ) ( y ) ) n \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \lim_{y \to x} (f(x)(y))^n ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ lim ( x , y ) → ( x , x ) f ( x , y ) n = ( lim y → x f ( x ) ( y ) ) n \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{y \to x} f(x)(y)\right)^n ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ lim ( x , y ) → ( x , x ) f ( x , y ) n = ( lim ( x , y ) → ( x , x ) f ( x , y ) ) n \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \lim_{(x, y) \to (x, x)} f(x, y)^n = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^n
Limits preserve reciprocals of functions
Where x − 1 x^{-1} is another notation for 1 x \frac{1}{x}
∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ ( lim ( x , y ) → ( x , x ) f ( x , y ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) − 1 = lim ( x , y ) → ( x , x ) ( f − 1 ) ( x , y ) ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{(x, y) \to (x, x)} (f^{-1})(x, y)\right) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ ( lim ( x , y ) → ( x , x ) f ( x , y ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) − 1 = lim y → x ( f − 1 ) ( x ) ( y ) ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f^{-1})(x)(y)\right) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ ( lim ( x , y ) → ( x , x ) f ( x , y ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) − 1 = lim y → x ( f ( x ) ( y ) ) − 1 ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \lim_{y \to x} (f(x)(y))^{-1}\right) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ ( lim ( x , y ) → ( x , x ) f ( x , y ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) − 1 = ( lim y → x f ( x ) ( y ) ) − 1 ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{y \to x} f(x)(y)\right)^{-1}\right) ∏ x : S ∏ f : DiagLimFunc ( S , F ) ∏ n : ℕ ( lim ( x , y ) → ( x , x ) f ( x , y ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) − 1 = ( lim ( x , y ) → ( x , x ) f ( x , y ) ) − 1 ) \prod_{x:S} \prod_{f:DiagLimFunc(S, F)} \prod_{n:\mathbb{N}} \left(\lim_{(x, y) \to (x, x)} f(x, y) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y)^{-1} = \left(\lim_{(x, y) \to (x, x)} f(x, y)\right)^{-1}\right)
Limits preserve that the reciprocals of functions are multiplicative inverses
Where x − 1 x^{-1} is another notation for 1 x \frac{1}{x}
∏ x : S ( ( lim x → c x ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ f ( x , y ) − 1 = lim ( x , y ) → ( x , x ) ( f ⋅ f − 1 ) ( x , y ) ) \prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{(x, y) \to (x, x)} (f \cdot f^{-1})(x, y)\right) ∏ x : S ( ( lim x → c x ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ f ( x , y ) − 1 = lim y → x ( f ⋅ f − 1 ) ( x ) ( y ) ) \prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} (f \cdot f^{-1})(x)(y)\right) ∏ x : S ( ( lim x → c x ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ f ( x , y ) − 1 = lim y → x f ( x ) ( y ) ⋅ f ( x ) ( y ) − 1 ) \prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = \lim_{y \to x} f(x)(y) \cdot {f(x)(y)}^{-1}\right) ∏ x : S ( ( lim x → c x ) # 0 ) → ( lim ( x , y ) → ( x , x ) f ( x , y ) ⋅ f ( x , y ) − 1 = 1 ) \prod_{x:S} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{(x, y) \to (x, x)} f(x, y) \cdot {f(x, y)}^{-1} = 1\right)
See also
Revision on April 16, 2022 at 14:59:12 by
Anonymous? .
See the history of this page for a list of all contributions to it.