IsPreconnected.eq_of_sq_eq
theorem IsPreconnected.eq_of_sq_eq :
β {Ξ± : Type u_2} {π : Type u_3} {f g : Ξ± β π} {S : Set Ξ±} [inst : TopologicalSpace Ξ±] [inst_1 : TopologicalSpace π]
[inst_2 : T1Space π] [inst_3 : Field π] [inst_4 : HasContinuousInvβ π] [inst_5 : ContinuousMul π],
IsPreconnected S β
ContinuousOn f S β
ContinuousOn g S β
Set.EqOn (f ^ 2) (g ^ 2) S β (β {x : Ξ±}, x β S β g x β 0) β β {y : Ξ±}, y β S β f y = g y β Set.EqOn f g S
This theorem states that if `f` and `g` are functions from a type `Ξ±` to a type `π`, both of which are continuous on a preconnected set `S`, and if `f` squared equals `g` squared on `S`, and `g` is never zero on `S`, then if `f` equals `g` at any single point in `S`, `f` and `g` are actually equal at every point in `S`. All these conditions are within the context where `Ξ±` and `π` are topological spaces, `π` is a T1 space and a field, and possesses continuous multiplicative inverses and multiplication.
More concisely: If `f` and `g` are continuous functions from a preconnected set `S` in topological spaces `Ξ±` and `π` (a T1 field with continuous multiplicative inverses), with `fΒ² = gΒ²` and `g β 0` on `S`, then `f = g` on `S` whenever `f(x) = g(x)` for some `x β S`.
|
Filter.tendsto_cocompact_mul_rightβ
theorem Filter.tendsto_cocompact_mul_rightβ :
β {K : Type u_1} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [inst_2 : ContinuousMul K] {a : K},
a β 0 β Filter.Tendsto (fun x => x * a) (Filter.cocompact K) (Filter.cocompact K)
This theorem states that in the context of a topological division ring `K`, given a nonzero element `a` of `K`, the function of right-multiplication by `a` has the property that the inverse image of any set whose complement is compact (described by the `Filter.cocompact K` filter) is also a set whose complement is compact. This property is often described by saying that the function is "proper". The requirement of `a` being nonzero is important because if `a` were zero, right-multiplication by `a` would map all elements of `K` to zero, which would not preserve compactness properties. The presence of `ContinuousMul K` in the context ensures that multiplication is a continuous operation in the topological space `K`.
More concisely: In a topological division ring `K`, the right multiplication by a nonzero element `a` is a proper continuous function, i.e., the inverse image of any compact set under right multiplication by `a` is a set with compact complement.
|
Filter.tendsto_cocompact_mul_leftβ
theorem Filter.tendsto_cocompact_mul_leftβ :
β {K : Type u_1} [inst : DivisionRing K] [inst_1 : TopologicalSpace K] [inst_2 : ContinuousMul K] {a : K},
a β 0 β Filter.Tendsto (fun x => a * x) (Filter.cocompact K) (Filter.cocompact K)
The theorem `Filter.tendsto_cocompact_mul_leftβ` states that for any division ring `K` equipped with a topology and a continuous multiplication operation, and for any non-zero element `a` of `K`, the left multiplication by `a` is a proper mapping with respect to the co-compact filter on `K`. In other words, if we take a co-compact set (i.e., the complement of a compact set) in `K`, and look at its image under the function `x β¦ ax`, this image is also co-compact. This implies that the preimage of any compact set under this left multiplication operation is also compact.
More concisely: For any division ring equipped with a topology and a continuous multiplication operation, the left multiplication by a non-zero element is a proper mapping with respect to the co-compact filter, preserving compact sets.
|
IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq
theorem IsPreconnected.eq_one_or_eq_neg_one_of_sq_eq :
β {Ξ± : Type u_2} {π : Type u_3} {f : Ξ± β π} {S : Set Ξ±} [inst : TopologicalSpace Ξ±] [inst_1 : TopologicalSpace π]
[inst_2 : T1Space π] [inst_3 : Ring π] [inst_4 : NoZeroDivisors π],
IsPreconnected S β ContinuousOn f S β Set.EqOn (f ^ 2) 1 S β Set.EqOn f 1 S β¨ Set.EqOn f (-1) S
The theorem states that if `f` is a function from a set `Ξ±` to a set `π` that remains continuous over a preconnected set `S`, and the square of `f` equals `1` within the set `S`, then the function `f` is either equal to `1` or `-1` throughout the set `S`. It's important to note that the function `f` maps any element in `Ξ±` to an element in `π`, `π` is assumed to be a topological space with the properties of a T1 space, a Ring, and includes no zero divisors. The condition for a set to be preconnected is that there is no non-trivial open partition. The continuity condition requires `f` to be continuous at every point in `S`. The equality condition checks that the function `f` is equal to either `1` or `-1` for all elements in `S`.
More concisely: If `f` is a continuous function from a preconnected set `S` in a T1 ring `π` with no zero divisors, such that `f(x)^2 = 1` for all `x` in `S`, then `f(x)` is constant to `1` or `-1` over `S`.
|
IsPreconnected.eq_or_eq_neg_of_sq_eq
theorem IsPreconnected.eq_or_eq_neg_of_sq_eq :
β {Ξ± : Type u_2} {π : Type u_3} {f g : Ξ± β π} {S : Set Ξ±} [inst : TopologicalSpace Ξ±] [inst_1 : TopologicalSpace π]
[inst_2 : T1Space π] [inst_3 : Field π] [inst_4 : HasContinuousInvβ π] [inst_5 : ContinuousMul π],
IsPreconnected S β
ContinuousOn f S β
ContinuousOn g S β
Set.EqOn (f ^ 2) (g ^ 2) S β (β {x : Ξ±}, x β S β g x β 0) β Set.EqOn f g S β¨ Set.EqOn f (-g) S
This theorem states that if `f` and `g` are functions from a set `Ξ±` to `π`, both continuous on a preconnected set `S`, and `f^2 = g^2` on `S`, and `g(z)` is not equal to 0 for all `z` in `S`, then either `f` is equal to `g` or `f` is equal to `-g` on `S`. This essentially means that when two continuous functions have their squares equal on a preconnected set and none of the function values of `g` on `S` are zero, the functions must be either the same or negatives of each other on that set.
More concisely: If `f` and `g` are continuous functions from a preconnected set `S` to the real numbers with `f^2 = g^2` on `S` and `g(z) β 0` for all `z` in `S`, then `f = g` or `f = -g` on `S`.
|