WithZeroTopology.singleton_mem_nhds_of_ne_zero
theorem WithZeroTopology.singleton_mem_nhds_of_ne_zero :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀}, γ ≠ 0 → {γ} ∈ nhds γ
The theorem `WithZeroTopology.singleton_mem_nhds_of_ne_zero` states that in the context of a linearly ordered commutative group with an adjoined zero element (denoted as `Γ₀`), if `γ` is a non-zero element of this group, then the set consisting of just `γ` (`{γ}`) is a neighborhood of `γ`. In other words, the singleton set containing `γ` is within the neighborhood filter of `γ` in the given topological space.
More concisely: In a linearly ordered commutative group with an adjoined zero element, the singleton set of a non-zero element is in the neighborhood filter of that element.
|
WithZeroTopology.t3Space
theorem WithZeroTopology.t3Space : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], T3Space Γ₀
This theorem states that for any type `Γ₀`, which is a linearly ordered commutative group with a zero element, the topology on this type is a T₃ space. In the context of topology, a T₃ space is a topological space in which any closed set and a point not contained in that set can be separated by two disjoint open sets.
More concisely: For any linearly ordered commutative group `Γ₀` with a zero element, its topology is a T₃ space.
|
WithZeroTopology.singleton_mem_nhds_of_units
theorem WithZeroTopology.singleton_mem_nhds_of_units :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), {↑γ} ∈ nhds ↑γ
The theorem `WithZeroTopology.singleton_mem_nhds_of_units` states that if `γ` is an invertible element (`Γ₀ˣ` denotes the group of units or invertible elements) of a linearly ordered commutative group with a zero element adjoined (`LinearOrderedCommGroupWithZero Γ₀`), then the set containing only `γ` (`{↑γ}`) is a neighborhood of `γ` in this topological space. In other words, for such group `Γ₀`, any unit `γ` is surrounded by an open set which is, in this case, the set `{↑γ}` itself.
More concisely: In a linearly ordered commutative group with a zero element, every invertible element is a neighborhood of itself.
|
WithZeroTopology.hasBasis_nhds_zero
theorem WithZeroTopology.hasBasis_nhds_zero :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], (nhds 0).HasBasis (fun γ => γ ≠ 0) Set.Iio
This theorem states that in a linearly ordered commutative group with a zero element adjoined (denoted as `Γ₀`), a set `U` is a neighborhood of `0` if and only if there exists a nonzero element `γ₀` such that all elements less than `γ₀` (expressed as `Iio γ₀`) are included in `U`. In other words, the neighborhood filter at `0` (`nhds 0`) has a basis consisting of left-infinite right-open intervals `Iio γ`, where `γ` is any nonzero element of the group.
More concisely: A neighborhood filter at the zero element in a linearly ordered commutative group has a basis consisting of left-infinite right-open intervals centered around nonzero elements.
|
WithZeroTopology.nhds_of_ne_zero
theorem WithZeroTopology.nhds_of_ne_zero :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {γ : Γ₀}, γ ≠ 0 → nhds γ = pure γ
This theorem states that in the context of a linearly ordered commutative group with zero, the neighborhood filter of a nonzero element consists only of sets containing that element. This means that any set that we consider as a 'neighborhood' of the element must contain the element itself, and this applies to all such elements that are not zero.
More concisely: In a linearly ordered commutative group with zero, the neighborhood filter of each nonzero element is equal to the filter generated by that element.
|
WithZeroTopology.nhds_coe_units
theorem WithZeroTopology.nhds_coe_units :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), nhds ↑γ = pure ↑γ
The theorem `WithZeroTopology.nhds_coe_units` declares that for any linear ordered commutative group with zero, denoted by `Γ₀`, and any invertible element `γ` of `Γ₀`, the neighborhood filter of `γ` (obtained using the `nhds` function) is equivalent to the singleton set consisting only of `γ` itself. In other words, the neighborhood of an invertible element in this mathematical structure consists of all sets that contain that particular element.
More concisely: For any linear ordered commutative group with zero `Γ₀` and invertible element `γ` in it, the neighborhood filter of `γ` is equal to the singleton set `{γ}`.
|
WithZeroTopology.nhds_zero_of_units
theorem WithZeroTopology.nhds_zero_of_units :
∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), Set.Iio ↑γ ∈ nhds 0
The theorem `WithZeroTopology.nhds_zero_of_units` states that for any given invertible element `γ` of a linearly ordered commutative group with a zero element adjoined (denoted as `Γ₀`), the set of all elements less than `γ` in `Γ₀` (represented as `Set.Iio ↑γ`) is a neighborhood of `0`. In other words, within this specific type of group, if you pick any invertible element, the set of all group elements that are less than this picked element forms a neighborhood around the zero element of the group.
More concisely: For any invertible element `γ` in a linearly ordered commutative group with a zero element, `Set.Iio ↑γ` is a neighborhood of `0`.
|