Homotopy Type Theory
limit of a binary function approaching a diagonal > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Contents
< limit of a binary function approaching a diagonal
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
Let U U be a type such that Δ # ( S ) ⊆ U \Delta_{\#}(S) \subseteq U and U ⊆ S × S U \subseteq S \times S . As a result, for every x : S x:S , there is a dependent type
U ( x ) ≔ ∑ y : S ( x , y ) U(x) \coloneqq \sum_{y:S} (x, y)
Given a partial binary function q : U → T q:U \to T , the currying of q q results in the dependent functions
x : S ⊢ q ( x ) : ( ∑ y : U ( x ) ( x , y ) ) → T x:S \vdash q(x): \left(\sum_{y:U(x)} (x,y)\right) \to T
A function g : S → T g:S \to T is a 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
hasLimitApproachingDiagonal ( q ) ≔ [ ∑ g : S → T ∏ x : S lim y → x q ( x ) ( y ) = g ( x ) ] hasLimitApproachingDiagonal(q) \coloneqq \left[\sum_{g:S \to T} \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 ) : DiagLimFunc ( S , T ) → ( S → F ) \lim_{(x, y) \to (x, x)} (-)(x, y): DiagLimFunc(S, T) \to (S \to F)
which returns the limit of a partial binary function q : DiagLimFunc ( S , T ) q:DiagLimFunc(S, T) approaching the diagonal and thus satisfies the equation
∏ 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 an algebraic limit 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 June 10, 2022 at 17:44:53 by
Anonymous? .
See the history of this page for a list of all contributions to it.