Normed fields #
In this file we continue building the theory of normed division rings and fields.
Some useful results that relate the topology of the normed field to the discrete topology include:
Multiplication by a nonzero element a on the left
as a DilationEquiv of a normed division ring.
Equations
- DilationEquiv.mulLeft a ha = { toEquiv := Equiv.mulLeft₀ a ha, edist_eq' := ⋯ }
Instances For
@[simp]
theorem
DilationEquiv.mulLeft_symm_apply
{α : Type u_1}
[NormedDivisionRing α]
(a : α)
(ha : a ≠ 0)
(x : α)
:
@[simp]
theorem
DilationEquiv.mulLeft_apply
{α : Type u_1}
[NormedDivisionRing α]
(a : α)
(ha : a ≠ 0)
(x : α)
:
Multiplication by a nonzero element a on the right
as a DilationEquiv of a normed division ring.
Equations
- DilationEquiv.mulRight a ha = { toEquiv := Equiv.mulRight₀ a ha, edist_eq' := ⋯ }
Instances For
@[simp]
theorem
DilationEquiv.mulRight_apply
{α : Type u_1}
[NormedDivisionRing α]
(a : α)
(ha : a ≠ 0)
(x : α)
:
@[simp]
theorem
DilationEquiv.mulRight_symm_apply
{α : Type u_1}
[NormedDivisionRing α]
(a : α)
(ha : a ≠ 0)
(x : α)
:
@[simp]
@[simp]
theorem
Filter.tendsto_mul_left_cobounded
{α : Type u_1}
[NormedDivisionRing α]
{a : α}
(ha : a ≠ 0)
:
Tendsto (fun (x : α) => a * x) (Bornology.cobounded α) (Bornology.cobounded α)
Multiplication on the left by a nonzero element of a normed division ring tends to infinity at infinity.
theorem
Filter.tendsto_mul_right_cobounded
{α : Type u_1}
[NormedDivisionRing α]
{a : α}
(ha : a ≠ 0)
:
Tendsto (fun (x : α) => x * a) (Bornology.cobounded α) (Bornology.cobounded α)
Multiplication on the right by a nonzero element of a normed division ring tends to infinity at infinity.
@[simp]
@[simp]
@[deprecated Filter.inv_nhdsNE_zero (since := "2025-11-26")]
Alias of Filter.inv_nhdsNE_zero.
theorem
Filter.tendsto_inv₀_cobounded'
{α : Type u_1}
[NormedDivisionRing α]
:
Tendsto Inv.inv (Bornology.cobounded α) (nhdsWithin 0 {0}ᶜ)
theorem
Filter.tendsto_inv₀_cobounded
{α : Type u_1}
[NormedDivisionRing α]
:
Tendsto Inv.inv (Bornology.cobounded α) (nhds 0)
theorem
Filter.tendsto_inv₀_nhdsNE_zero
{α : Type u_1}
[NormedDivisionRing α]
:
Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
@[deprecated Filter.tendsto_inv₀_nhdsNE_zero (since := "2025-11-26")]
theorem
Filter.tendsto_inv₀_nhdsWithin_ne_zero
{α : Type u_1}
[NormedDivisionRing α]
:
Tendsto Inv.inv (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
Alias of Filter.tendsto_inv₀_nhdsNE_zero.
theorem
uniformContinuousOn_inv₀
{α : Type u_1}
[NormedDivisionRing α]
{s : Set α}
(hs : sᶜ ∈ nhds 0)
:
If s is a set disjoint from 𝓝 0, then fun x ↦ x⁻¹ is uniformly continuous on s.
theorem
UniformContinuousOn.inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
[UniformSpace X]
{f : X → α}
{s : Set X}
(hf : UniformContinuousOn f s)
(hf₀ : (f '' s)ᶜ ∈ nhds 0)
:
theorem
UniformContinuousOn.fun_inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
[UniformSpace X]
{f : X → α}
{s : Set X}
(hf : UniformContinuousOn f s)
(hf₀ : (f '' s)ᶜ ∈ nhds 0)
:
UniformContinuousOn (fun (i : X) => (f i)⁻¹) s
Eta-expanded form of UniformContinuousOn.inv₀
theorem
UniformContinuous.inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
[UniformSpace X]
{f : X → α}
(hf : UniformContinuous f)
(hf₀ : (Set.range f)ᶜ ∈ nhds 0)
:
theorem
UniformContinuous.fun_inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
[UniformSpace X]
{f : X → α}
(hf : UniformContinuous f)
(hf₀ : (Set.range f)ᶜ ∈ nhds 0)
:
UniformContinuous fun (i : X) => (f i)⁻¹
Eta-expanded form of UniformContinuous.inv₀
theorem
TendstoLocallyUniformlyOn.inv₀_of_disjoint
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hf : ∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0))
:
TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
theorem
TendstoLocallyUniformlyOn.fun_inv₀_of_disjoint
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hf : ∀ x ∈ s, Disjoint (Filter.map f (nhdsWithin x s)) (nhds 0))
:
TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l s
Eta-expanded form of TendstoLocallyUniformlyOn.inv₀_of_disjoint
theorem
TendstoLocallyUniformly.inv₀_of_disjoint
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hf : ∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0))
:
theorem
TendstoLocallyUniformly.fun_inv₀_of_disjoint
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hf : ∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0))
:
TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l
Eta-expanded form of TendstoLocallyUniformly.inv₀_of_disjoint
theorem
TendstoLocallyUniformlyOn.inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hf : ContinuousOn f s)
(hf₀ : ∀ x ∈ s, f x ≠ 0)
:
TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
theorem
TendstoLocallyUniformlyOn.fun_inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hf : ContinuousOn f s)
(hf₀ : ∀ x ∈ s, f x ≠ 0)
:
TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l s
Eta-expanded form of TendstoLocallyUniformlyOn.inv₀
theorem
TendstoLocallyUniformly.inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hf : Continuous f)
(hf₀ : ∀ (x : X), f x ≠ 0)
:
theorem
TendstoLocallyUniformly.fun_inv₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F : ι → X → α}
{f : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hf : Continuous f)
(hf₀ : ∀ (x : X), f x ≠ 0)
:
TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => (F i i_1)⁻¹) (fun (i : X) => (f i)⁻¹) l
Eta-expanded form of TendstoLocallyUniformly.inv₀
@[instance 100]
@[deprecated NormedDivisionRing.to_continuousInv₀ (since := "2025-09-01")]
Alias of NormedDivisionRing.to_continuousInv₀.
theorem
TendstoLocallyUniformlyOn.div₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F G : ι → X → α}
{f g : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hG : TendstoLocallyUniformlyOn G g l s)
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
(hg₀ : ∀ x ∈ s, g x ≠ 0)
:
TendstoLocallyUniformlyOn (F / G) (f / g) l s
theorem
TendstoLocallyUniformlyOn.fun_div₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{s : Set X}
{F G : ι → X → α}
{f g : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformlyOn F f l s)
(hG : TendstoLocallyUniformlyOn G g l s)
(hf : ContinuousOn f s)
(hg : ContinuousOn g s)
(hg₀ : ∀ x ∈ s, g x ≠ 0)
:
TendstoLocallyUniformlyOn (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l s
Eta-expanded form of TendstoLocallyUniformlyOn.div₀
theorem
TendstoLocallyUniformly.div₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F G : ι → X → α}
{f g : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hG : TendstoLocallyUniformly G g l)
(hf : Continuous f)
(hg : Continuous g)
(hg₀ : ∀ (x : X), g x ≠ 0)
:
TendstoLocallyUniformly (F / G) (f / g) l
theorem
TendstoLocallyUniformly.fun_div₀
{α : Type u_1}
[NormedDivisionRing α]
{X : Type u_4}
{ι : Type u_5}
[TopologicalSpace X]
{F G : ι → X → α}
{f g : X → α}
{l : Filter ι}
(hF : TendstoLocallyUniformly F f l)
(hG : TendstoLocallyUniformly G g l)
(hf : Continuous f)
(hg : Continuous g)
(hg₀ : ∀ (x : X), g x ≠ 0)
:
TendstoLocallyUniformly (fun (i : ι) (i_1 : X) => F i i_1 / G i i_1) (fun (i : X) => f i / g i) l
Eta-expanded form of TendstoLocallyUniformly.div₀
@[instance 100]
A normed division ring is a topological division ring.
theorem
tendsto_norm_inv_nhdsNE_zero_atTop
{α : Type u_1}
[NormedDivisionRing α]
:
Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop
@[deprecated tendsto_norm_inv_nhdsNE_zero_atTop (since := "2025-11-26")]
theorem
NormedField.tendsto_norm_inv_nhdsNE_zero_atTop
{α : Type u_1}
[NormedDivisionRing α]
:
Filter.Tendsto (fun (x : α) => ‖x⁻¹‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop
Alias of tendsto_norm_inv_nhdsNE_zero_atTop.
theorem
tendsto_zpow_nhdsNE_zero_cobounded
{α : Type u_1}
[NormedDivisionRing α]
{m : ℤ}
(hm : m < 0)
:
Filter.Tendsto (fun (x : α) => x ^ m) (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
@[deprecated tendsto_zpow_nhdsNE_zero_cobounded (since := "2025-11-26")]
theorem
NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop
{α : Type u_1}
[NormedDivisionRing α]
{m : ℤ}
(hm : m < 0)
:
Filter.Tendsto (fun (x : α) => ‖x ^ m‖) (nhdsWithin 0 {0}ᶜ) Filter.atTop
theorem
NormedField.discreteTopology_or_nontriviallyNormedField
(𝕜 : Type u_4)
[h : NormedField 𝕜]
:
A normed field is either nontrivially normed or has a discrete topology.
In the discrete topology case, all the norms are 1, by norm_eq_one_iff_ne_zero_of_discrete.
The nontrivially normed field instance is provided by a subtype with a proof that the
forgetful inheritance to the existing NormedField instance is definitionally true.
This allows one to have the new NontriviallyNormedField instance without data clashes.
theorem
NormedField.discreteTopology_of_bddAbove_range_norm
{𝕜 : Type u_4}
[NormedField 𝕜]
(h : BddAbove (Set.range fun (k : 𝕜) => ‖k‖))
:
@[simp]
@[simp]
Equations
- Rat.instNormedField = { toNorm := Rat.instNormedAddCommGroup.toNorm, toField := Rat.instField, toMetricSpace := Rat.instNormedAddCommGroup.toMetricSpace, dist_eq := ⋯, norm_mul := ⋯ }
Equations
- Rat.instDenselyNormedField = { toNormedField := Rat.instNormedField, lt_norm_lt := Rat.instDenselyNormedField._proof_1 }