LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Topology.Algebra.Module.FiniteDimension

`LinearMap.isOpenMap_of_finiteDimensional` theorem LinearMap.isOpenMap_of_finiteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : TopologicalAddGroup F] [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E] (f : F →ₗ[𝕜] E), Function.Surjective ⇑f → IsOpenMap ⇑f The theorem `LinearMap.isOpenMap_of_finiteDimensional` states that a surjective linear map `f` from one topological vector space to another, where the codomain is a finite-dimensional topological vector space, is an open map. In other words, for any open set in the domain, its image under `f` is open in the codomain. This theorem requires the codomain to be finite-dimensional and the map to be surjective. In the context of topology, this kind of theorem helps to characterize the behavior of continuous, linear transformations between topological vector spaces. More concisely: A surjective linear map between topological vector spaces sends open sets to open sets if and only if the codomain is finite-dimensional.
`closedEmbedding_smul_left` theorem closedEmbedding_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : T2Space E] [inst_5 : TopologicalAddGroup E] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] {c : E}, c ≠ 0 → ClosedEmbedding fun x => x • c This theorem states that for any non-zero element `c` in a certain type `E`, the function that multiplies `c` by a scalar `x` is a closed embedding. Here, `𝕜` is a nontrivially normed field that is also complete, `E` is an additive group with a topological structure satisfying the T2 property and is also a topological additive group. Additionally, `E` is a module over `𝕜` and the scalar multiplication in this module is continuous. A closed embedding in this context implies that the function is both injective and continuous, and its image is a closed set in the codomain. More concisely: For any non-zero `c` in the topological module `E` over a complete, nontrivially normed field `𝕜`, the scalar multiplication function `x mapsto c * x` is a continuous, injective and closed embedding.
`FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq` theorem FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : TopologicalAddGroup F] [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F] [inst_13 : FiniteDimensional 𝕜 E] [inst_14 : FiniteDimensional 𝕜 F], Nonempty (E ≃L[𝕜] F) ↔ FiniteDimensional.finrank 𝕜 E = FiniteDimensional.finrank 𝕜 F The theorem `FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq` states that for two finite-dimensional topological vector spaces E and F over a complete normed field 𝕜, there exists a continuous linear equivalence between E and F if and only if both E and F have the same finite dimension. In other words, two such vector spaces are continuously linearly equivalent if their dimensions, as computed by `FiniteDimensional.finrank`, are equal. More concisely: Two finite-dimensional topological vector spaces over a complete normed field are continuously linearly equivalent if and only if they have equal finite dimensions.
`FiniteDimensional.complete` theorem FiniteDimensional.complete : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : UniformSpace E] [inst_4 : T2Space E] [inst_5 : UniformAddGroup E] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] [inst : FiniteDimensional 𝕜 E], CompleteSpace E This theorem states that, for any non-trivially normed field 𝕜 and any type E, given that 𝕜 is a complete space, E is an additive commutative group, E is a uniform space, E is a T2 space (also known as a Hausdorff space), E is a uniform additive group, 𝕜 is a module for E, 𝕜 scalar multiplication on E is continuous, and E is a finite-dimensional 𝕜-vector space, then E is a complete space. In simpler terms, it states that any finite-dimensional vector space over a complete field is itself a complete space. More concisely: A finite-dimensional vector space over a complete field is a complete space.
`Submodule.complete_of_finiteDimensional` theorem Submodule.complete_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : UniformSpace E] [inst_4 : T2Space E] [inst_5 : UniformAddGroup E] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] (s : Submodule 𝕜 E) [inst_8 : FiniteDimensional 𝕜 ↥s], IsComplete ↑s This theorem states that a finite-dimensional subspace is complete. More specifically, for any nontrivially normed field 𝕜 and any type E that forms a complete space over 𝕜, a uniform space, a T2 space, a uniform additive group, and a module over 𝕜, if we consider a submodule s of E, which is finite-dimensional over 𝕜, then s is a complete set. In the context of metric spaces, this means that for any Cauchy filter `f` on s, there exists an element `x` in s such that `f` is eventually within any given neighborhood of `x`. More concisely: A finite-dimensional subspace of a complete normed field is a complete subspace.
`LinearMap.continuous_iff_isClosed_ker` theorem LinearMap.continuous_iff_isClosed_ker : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜), Continuous ⇑l ↔ IsClosed ↑(LinearMap.ker l) This theorem states that for any linear form (represented as 'l') on a topological vector space 'E' over a nontrivially normed field '𝕜', the continuity of the linear form is equivalent to the closure of its kernel. Here, 'E' is a group under addition, a module over the field '𝕜', a topological space, and a topological group under addition. The scalar multiplication in 'E' is also assumed to be continuous. Essentially, the theorem establishes a condition for the continuity of a linear form in terms of the properties of its kernel, specifically its closure. More concisely: For a linear form 'l' on a topological vector space 'E' over a normed field '𝕜', the kernel of 'l' is closed if and only if 'l' is continuous.
`LinearMap.continuous_of_isClosed_ker` theorem LinearMap.continuous_of_isClosed_ker : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜), IsClosed ↑(LinearMap.ker l) → Continuous ⇑l This theorem states that for any linear form on a topological vector space over a nontrivially normed field, if the kernel of the linear form is closed, then the linear form is continuous. Here, a nontrivially normed field is a field with a vector norm that isn't trivial, a topological vector space is a vector space equipped with a topological structure, and the kernel of a linear form is the set of vectors that map to zero. More concisely: If a linear form on a topological vector space over a nontrivially normed field has a closed kernel, then the linear form is continuous.
`Submodule.closed_of_finiteDimensional` theorem Submodule.closed_of_finiteDimensional : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : T2Space E] [inst_5 : TopologicalAddGroup E] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] (s : Submodule 𝕜 E) [inst_8 : FiniteDimensional 𝕜 ↥s], IsClosed ↑s The theorem `Submodule.closed_of_finiteDimensional` states that for any given nontrivial normed field `𝕜` and any given type `E` that forms a topological space, an additive group, a T2 space, and a topological additive group, which is also a module over `𝕜`, and where scalar multiplication is continuous, if we have a subspace `s` of `E` that forms a finite-dimensional vector space, then this subspace is closed in the topological space sense. In other words, a finite-dimensional subspace of a complete space over a given field is always a closed set. More concisely: A finite-dimensional subspace of a complete normed vector space is closed.
`LinearMap.continuous_of_nonzero_on_open` theorem LinearMap.continuous_of_nonzero_on_open : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜) (s : Set E), IsOpen s → s.Nonempty → (∀ x ∈ s, l x ≠ 0) → Continuous ⇑l This theorem states that for any nontrivially normed field `𝕜` and an additive commutative group `E` that is a `𝕜`-module and a topological space, if you have a linear map `l` from `E` to `𝕜`, and an open set `s` in `E` that is nonempty and on which the linear map `l` is nonzero, then the linear map `l` is continuous. This theorem links the concepts of linear maps, topological spaces, and continuity in the context of normed fields and modules. More concisely: If `l` is a nonzero linear map from the `𝕜`-module and topological space `E` to a nontrivially normed field `𝕜`, and `s` is a nonempty open subset of `E` on which `l` is nonzero, then `l` is continuous.
`continuous_equivFun_basis` theorem continuous_equivFun_basis : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] {ι : Type u_1} [inst_7 : Finite ι] (ξ : Basis ι 𝕜 E), Continuous ⇑ξ.equivFun This theorem states that for a non-discrete complete normed field, identified as `𝕜`, alongside a finite-dimensional topological vector space `E` over this field, the canonical identification (using a basis `ξ`) with the n-dimensional algebra over the field (`𝕜^n`) is a continuous function. This identification is conducted using the product topology. The importance of this theorem lies in its application, where it enables all linear maps from a T2 finite-dimensional topological vector space over `𝕜` to be continuous. This continuity, in turn, implies that all norms are equivalent in finite dimensions. More concisely: For a non-discrete complete normed field `𝕜` and a finite-dimensional topological vector space `E` over `𝕜` identified with `𝕜^n` using a basis `ξ`, this identification is a continuous function under the product topology.
`LinearMap.closedEmbedding_of_injective` theorem LinearMap.closedEmbedding_of_injective : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : T2Space E] [inst_5 : TopologicalAddGroup E] [inst_6 : Module 𝕜 E] [inst_7 : ContinuousSMul 𝕜 E] [inst_8 : AddCommGroup F] [inst_9 : TopologicalSpace F] [inst_10 : T2Space F] [inst_11 : TopologicalAddGroup F] [inst_12 : Module 𝕜 F] [inst_13 : ContinuousSMul 𝕜 F] [inst_14 : FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F}, LinearMap.ker f = ⊥ → ClosedEmbedding ⇑f The theorem `LinearMap.closedEmbedding_of_injective` states that for any injective linear map `f` from a topological vector space `E` over a non-trivial normed field `𝕜` to another topological vector space `F` over the same field, where `E` is finite-dimensional, the map `f` is a closed embedding. In other words, if `E` is a finite-dimensional space, and `f` is a linear map that has zero kernel (hence is injective), then the image of `f` is a closed subset of the codomain and `f` is a homeomorphism onto its image. More concisely: A finite-dimensional, injective linear map between topological vector spaces over a non-trivial normed field is a closed embedding and a homeomorphism onto its image.
`FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq` theorem FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w} [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : TopologicalAddGroup F] [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F] [inst_13 : FiniteDimensional 𝕜 E] [inst_14 : FiniteDimensional 𝕜 F], FiniteDimensional.finrank 𝕜 E = FiniteDimensional.finrank 𝕜 F → Nonempty (E ≃L[𝕜] F) The theorem `FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq` states that for any two finite-dimensional topological vector spaces `E` and `F` over a complete normed field `𝕜`, if they have the same finite dimension, then there exists a continuous linear equivalence between them. This means they can be mapped onto each other via a linear transformation that has a continuous inverse, preserving the vector space structure and topology. More concisely: Given two finite-dimensional topological vector spaces E and F over a complete normed field ℝ, if their dimensions are equal, then there exists a continuous linear bijective map between them with a continuous inverse.
`LinearMap.continuous_of_finiteDimensional` theorem LinearMap.continuous_of_finiteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E] [inst_3 : TopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F' : Type x} [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [inst_8 : TopologicalAddGroup F'] [inst_9 : ContinuousSMul 𝕜 F'] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] F'), Continuous ⇑f This theorem states that any linear map `f` from a vector space `E` to another space `F'`, where both `E` and `F'` are over the same complete field `𝕜`, is continuous. The vector space `E` is assumed to be finite-dimensional, topological, and a topological add group with continuous scalar multiplication. The space `F'` is also assumed to be topological and a topological add group with continuous scalar multiplication. The field `𝕜` is assumed to be a complete space with nontrivial norms. More concisely: Any finite-dimensional linear map between topological vector spaces over a complete field with continuous scalar multiplication is continuous.
`unique_topology_of_t2` theorem unique_topology_of_t2 : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {t : TopologicalSpace 𝕜}, TopologicalAddGroup 𝕜 → ContinuousSMul 𝕜 𝕜 → T2Space 𝕜 → t = UniformSpace.toTopologicalSpace This theorem states that for any type `𝕜` which is a nontrivially normed field, and any T2 topology (a topology where any two distinct points have disjoint open neighbourhoods) on `𝕜` which makes `𝕜` a topological vector space over itself with respect to the norm topology, this T2 topology is equal to the topology derived from the uniform space structure on `𝕜`. In other words, if a normed field is endowed with a T2 topology that's compatible with its linear structure and multiplication, then this topology is the same as the one induced by the uniform structure generated by the norm. More concisely: For any nontrivially normed field `𝕜` with a T2 topology making it a topological vector space, this topology equals the topology derived from its uniform space structure induced by the norm.