continuum_le_cardinal_of_module
theorem continuum_le_cardinal_of_module :
โ (๐ : Type u) (E : Type v) [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐] [inst_2 : AddCommGroup E]
[inst : Module ๐ E] [inst : Nontrivial E], Cardinal.continuum โค Cardinal.mk E
This theorem states that for any type `๐` and `E` where `๐` is a nontrivially normed field and complete space, and `E` is a module over `๐` with an additional structure of an additive commutative group and is nontrivial, the cardinality of `E` is at least as large as the cardinality of the continuum. The cardinality of the continuum, denoted as `Cardinal.continuum`, represents the size of the set of real numbers, and is equivalent to $2^{\aleph_0}$. Here, `aleph0` represents the cardinality of the set of natural numbers. Thus, this theorem is concerned with a lower bound on the size of the module `E`.
More concisely: For any nontrivially normed and complete field `๐` and module `E` over `๐` with additional structure of an additive commutative group and nontrivial, the cardinality of `E` is greater than or equal to the cardinality of the continuum.
|
cardinal_eq_of_isOpen
theorem cardinal_eq_of_isOpen :
โ {E : Type u_1} (๐ : Type u_2) [inst : NontriviallyNormedField ๐] [inst_1 : AddCommGroup E] [inst_2 : Module ๐ E]
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst : ContinuousSMul ๐ E] {s : Set E},
IsOpen s โ s.Nonempty โ Cardinal.mk โs = Cardinal.mk E
The theorem `cardinal_eq_of_isOpen` states that in a topological vector space `E` over a nontrivially normed field `๐`, if we have a nonempty open set `s`, then the cardinality of this set `s` is the same as the cardinality of the whole space `E`. This means that, despite their apparent difference in "size", the open set `s` and the entire space `E` have the same number of elements. This is a powerful result in the theory of infinite sets and it relies on the topological and algebraic structure of the space `E`.
More concisely: In a nonempty open set of a topological vector space over a nontrivially normed field, the cardinality is equal to that of the entire space.
|
Set.Countable.dense_compl
theorem Set.Countable.dense_compl :
โ {E : Type u} (๐ : Type u_1) [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : AddCommGroup E] [inst_3 : Module ๐ E] [inst_4 : Nontrivial E] [inst_5 : TopologicalSpace E]
[inst_6 : ContinuousAdd E] [inst : ContinuousSMul ๐ E] {s : Set E}, s.Countable โ Dense sแถ
This theorem states that in a nontrivial topological vector space over a complete, nontrivially normed field, the complement of any countable set is dense. Here, a set is nontrivial if it contains at least two distinct elements, a field is normed if it has a notion of size or length for its elements, a topological vector space is a vector space equipped with a topology that allows for the notion of continuity, and a set is dense if every point in the space is either in the set or can be approximated by points in the set. A set's complement consists of all elements not in the set, and a set is countable if its elements can be put into one-to-one correspondence with the set of natural numbers.
More concisely: In a nontrivial topological vector space over a complete, normed field, the complement of any countable set is dense.
|
cardinal_eq_of_mem_nhds
theorem cardinal_eq_of_mem_nhds :
โ {E : Type u_1} (๐ : Type u_2) [inst : NontriviallyNormedField ๐] [inst_1 : AddCommGroup E] [inst_2 : Module ๐ E]
[inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst : ContinuousSMul ๐ E] {s : Set E} {x : E},
s โ nhds x โ Cardinal.mk โs = Cardinal.mk E
This theorem states that in a topological vector space over a field which is nontrivially normed, any neighborhood of a point has the same cardinality as the whole space. In more detail, given a type `E` that has the structure of an additive commutative group, a module over a nontrivially normed field `๐`, and a topological space with continuous addition and scalar multiplication, for any set `s` which is a neighborhood of a point `x` in `E`, the cardinality of `s` is equal to the cardinality of `E`. That is, in such a mathematical structure, any neighborhood of a point, no matter how small, has the same 'size' or number of elements as the entire space.
More concisely: In a topological vector space over a nontrivially normed field, any neighborhood of a point has the same cardinality as the entire space.
|
continuum_le_cardinal_of_isOpen
theorem continuum_le_cardinal_of_isOpen :
โ {E : Type u_1} (๐ : Type u_2) [inst : NontriviallyNormedField ๐] [inst_1 : CompleteSpace ๐]
[inst_2 : AddCommGroup E] [inst_3 : Module ๐ E] [inst_4 : Nontrivial E] [inst_5 : TopologicalSpace E]
[inst_6 : ContinuousAdd E] [inst : ContinuousSMul ๐ E] {s : Set E},
IsOpen s โ s.Nonempty โ Cardinal.continuum โค Cardinal.mk โs
The theorem `continuum_le_cardinal_of_isOpen` asserts that in any nontrivial topological vector space `E` over a complete nontrivially normed field `๐`, if `s` is a nonempty open set in `E`, then the cardinality (i.e., the size) of `s` is at least as large as the cardinality of the continuum. The continuum, denoted by `Cardinal.continuum`, is the cardinality of the real numbers, which is equal to the cardinality of the power set of the natural numbers (i.e., `2^aleph0`).
In simpler terms, the theorem states that any nonempty open set in such a space cannot have less elements than the set of real numbers.
More concisely: In any nontrivial topological vector space over a complete nontrivially normed field, the cardinality of any nonempty open set is greater than or equal to the cardinality of the continuum.
|
continuum_le_cardinal_of_nontriviallyNormedField
theorem continuum_le_cardinal_of_nontriviallyNormedField :
โ (๐ : Type u_1) [inst : NontriviallyNormedField ๐] [inst : CompleteSpace ๐], Cardinal.continuum โค Cardinal.mk ๐
The theorem `continuum_le_cardinal_of_nontriviallyNormedField` states that for any type `๐` that is a complete nontrivially normed field, the cardinality of `๐` is at least the cardinality of the continuum. Here, the cardinality of the continuum is defined as the cardinality of the set of all real numbers, which is equivalent to $2^{|\aleph_0|}$, where $|\aleph_0|$ denotes the cardinality of the set of natural numbers. A nontrivially normed field is a field equipped with a norm (a function that assigns a non-negative length or size to each vector in a vector space) that distinguishes between different elements, meaning that the norm of an element is zero if and only if the element itself is zero. The term 'complete' in the context of a normed field means that every Cauchy sequence (a sequence where the distance between elements can be made arbitrarily small) converges to a limit in the field.
More concisely: The cardinality of a complete, nontrivially normed field is greater than or equal to the cardinality of the real numbers.
|
cardinal_eq_of_mem_nhds_zero
theorem cardinal_eq_of_mem_nhds_zero :
โ {E : Type u_1} (๐ : Type u_2) [inst : NontriviallyNormedField ๐] [inst_1 : AddCommGroup E] [inst_2 : Module ๐ E]
[inst_3 : TopologicalSpace E] [inst : ContinuousSMul ๐ E] {s : Set E},
s โ nhds 0 โ Cardinal.mk โs = Cardinal.mk E
This theorem states that in a topological vector space over a nontrivially normed field, the cardinality of any neighborhood of zero is the same as the cardinality of the entire space. Here, a topological vector space is a vector space that is also a topological space, and a nontrivially normed field is a field that has a norm defined in a certain way. A neighborhood of zero is a set that contains an open set around zero. The theorem asserts that if a set is a neighborhood of zero (i.e., `s โ nhds 0`), then the cardinality of the set (`Cardinal.mk โs`) equals the cardinality of the entire space (`Cardinal.mk E`).
More concisely: In a topological vector space over a nontrivially normed field, the cardinality of any neighborhood of zero is equal to the cardinality of the entire space.
|