Valued.hasBasis_nhds_zero
theorem Valued.hasBasis_nhds_zero :
∀ (R : Type u) [inst : Ring R] (Γ₀ : Type v) [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
(nhds 0).HasBasis (fun x => True) fun γ => {x | Valued.v x < ↑γ}
This theorem states that for any type `R` with a ring structure, and any type `Γ₀` with a structure of a linearly ordered commutative group with zero, if `R` is valued with `Γ₀`, then the neighborhood filter of zero in `R` has a basis. This basis is characterized by sets of elements `x` in `R` such that the valuation of `x` is less than a given element `γ` in `Γ₀`. In other words, it states that neighborhoods of zero in a valued ring can be characterized by the valuation being less than some threshold.
More concisely: In a valued ring with a linearly ordered commutative group of values, the neighborhood filter of zero has a basis consisting of elements with valuation less than any given value in the group.
|
Valued.mem_nhds
theorem Valued.mem_nhds :
∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
{s : Set R} {x : R}, s ∈ nhds x ↔ ∃ γ, {y | Valued.v (y - x) < ↑γ} ⊆ s
This theorem, `Valued.mem_nhds`, states that for any ring `R` and a linearly ordered commutative group with zero `Γ₀`, if the ring `R` is valued with `Γ₀`, then for any set `s` of type `R` and any element `x` of type `R`, the set `s` is a neighborhood of `x` if and only if there exists a γ in `Γ₀` such that the set containing all elements `y` in `R` whose value (given by the valuation `Valued.v`) of the difference between `y` and `x` is less than γ, is a subset of `s`. In other words, `s` is a neighborhood of `x` if it contains an open set around `x`, defined by a certain valuation condition.
More concisely: For a ring valued with a linearly ordered commutative group, a set is a neighborhood of an element if and only if it contains an open ball around that element defined by a certain valuation condition.
|
Valuation.subgroups_basis
theorem Valuation.subgroups_basis :
∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀),
RingSubgroupsBasis fun γ => v.ltAddSubgroup γ
This theorem asserts that for any ring `R` and any `Γ₀` which is a linearly ordered commutative group with zero, given any valuation `v` from `R` to `Γ₀`, the set of subgroups of `R` which consist of elements whose valuation is less than a certain unit form a basis for the topology on the ring `R` determined by the valuation `v`. This means that each open set in this topological space can be represented as a union of these subgroups.
More concisely: For any ring `R` and linearly ordered commutative group with zero `Γ₀`, the subgroups of `R` consisting of elements with valuation less than a fixed unit form a basis for the topology on `R` determined by any valuation from `R` to `Γ₀`.
|