(Semi)normed groups: basic theory

We prove basic properties of (semi)normed groups.

Tags

normed group

theorem dist_eq_norm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b = ‖a⁻¹ * b‖

theorem dist_eq_norm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖-a + b‖

theorem dist_eq_norm_inv_mul' {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b = ‖b⁻¹ * a‖

theorem dist_eq_norm_neg_add' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖-b + a‖

theorem DiscreteTopology.of_forall_le_norm' {E : Type u_5} [SeminormedGroup E] {r : ℝ} (hpos : 0 < r) (hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖) : DiscreteTopology E

theorem DiscreteTopology.of_forall_le_norm {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (hpos : 0 < r) (hr : ∀ (x : E), x ≠ 0 → r ≤ ‖x‖) : DiscreteTopology E

@[simp]

theorem dist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : dist a 1 = ‖a‖

@[simp]

theorem dist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist a 0 = ‖a‖

theorem inseparable_one_iff_norm {E : Type u_5} [SeminormedGroup E] {a : E} : Inseparable a 1 ↔ ‖a‖ = 0

theorem inseparable_zero_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a : E} : Inseparable a 0 ↔ ‖a‖ = 0

theorem dist_one_left {E : Type u_5} [SeminormedGroup E] (a : E) : dist 1 a = ‖a‖

theorem dist_zero_left {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist 0 a = ‖a‖

@[simp]

theorem dist_one {E : Type u_5} [SeminormedGroup E] : dist 1 = norm

@[simp]

theorem dist_zero {E : Type u_5} [SeminormedAddGroup E] : dist 0 = norm

theorem norm_div_rev {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖ = ‖b / a‖

theorem norm_sub_rev {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ = ‖b - a‖

@[simp]

theorem norm_inv' {E : Type u_5} [SeminormedGroup E] (a : E) : ‖a⁻¹‖ = ‖a‖

@[simp]

theorem norm_neg {E : Type u_5} [SeminormedAddGroup E] (a : E) : ‖-a‖ = ‖a‖

@[simp]

theorem norm_zpow_abs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ |n|‖ = ‖a ^ n‖

@[simp]

theorem norm_abs_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖|n| • a‖ = ‖n • a‖

@[simp]

theorem norm_pow_natAbs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖

@[simp]

theorem norm_natAbs_smul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖n.natAbs • a‖ = ‖n • a‖

theorem norm_zpow_isUnit {E : Type u_5} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖

theorem norm_isUnit_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖n • a‖ = ‖a‖

@[simp]

theorem norm_units_zsmul {E : Type u_8} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖ = ‖a‖

theorem dist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖

theorem dist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : dist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖

theorem norm_mul_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a * b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_add_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a + b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_mul_le_of_le' {E : Type u_5} [SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ + r₂

Triangle inequality for the norm.

theorem norm_add_le_of_le {E : Type u_5} [SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ + a₂‖ ≤ r₁ + r₂

Triangle inequality for the norm.

theorem norm_mul₃_le' {E : Type u_5} [SeminormedGroup E] {a b c : E} : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_add₃_le {E : Type u_5} [SeminormedAddGroup E] {a b c : E} : ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_mul₄_le' {E : Type u_5} [SeminormedGroup E] {a b c d : E} : ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖

Triangle inequality for the norm.

theorem norm_add₄_le {E : Type u_5} [SeminormedAddGroup E] {a b c d : E} : ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖

Triangle inequality for the norm.

theorem norm_div_le_norm_div_add_norm_div {E : Type u_5} [SeminormedGroup E] (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

theorem norm_sub_le_norm_sub_add_norm_sub {E : Type u_5} [SeminormedAddGroup E] (a b c : E) : ‖a - c‖ ≤ ‖a - b‖ + ‖b - c‖

theorem norm_le_norm_div_add {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖ ≤ ‖a / b‖ + ‖b‖

theorem norm_le_norm_sub_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖ ≤ ‖a - b‖ + ‖b‖

@[simp]

theorem norm_nonneg' {E : Type u_5} [SeminormedGroup E] (a : E) : 0 ≤ ‖a‖

@[simp]

theorem norm_nonneg {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖

@[simp]

theorem abs_norm' {E : Type u_5} [SeminormedGroup E] (z : E) : |‖z‖| = ‖z‖

@[simp]

theorem abs_norm {E : Type u_5} [SeminormedAddGroup E] (z : E) : |‖z‖| = ‖z‖

@[simp]

theorem norm_one' {E : Type u_5} [SeminormedGroup E] : ‖1‖ = 0

@[simp]

theorem norm_zero {E : Type u_5} [SeminormedAddGroup E] : ‖0‖ = 0

theorem ne_one_of_norm_ne_zero {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖ ≠ 0 → a ≠ 1

theorem ne_zero_of_norm_ne_zero {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖ ≠ 0 → a ≠ 0

theorem norm_of_subsingleton' {E : Type u_5} [SeminormedGroup E] [Subsingleton E] (a : E) : ‖a‖ = 0

theorem norm_of_subsingleton {E : Type u_5} [SeminormedAddGroup E] [Subsingleton E] (a : E) : ‖a‖ = 0

theorem zero_lt_one_add_norm_sq' {E : Type u_5} [SeminormedGroup E] (x : E) : 0 < 1 + ‖x‖ ^ 2

theorem zero_lt_one_add_norm_sq {E : Type u_5} [SeminormedAddGroup E] (x : E) : 0 < 1 + ‖x‖ ^ 2

theorem norm_div_le {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖ ≤ ‖a‖ + ‖b‖

theorem norm_sub_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ ≤ ‖a‖ + ‖b‖

theorem norm_div_le_of_le {E : Type u_5} [SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ / a₂‖ ≤ r₁ + r₂

theorem norm_sub_le_of_le {E : Type u_5} [SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ - a₂‖ ≤ r₁ + r₂

theorem dist_le_norm_add_norm' {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b ≤ ‖a‖ + ‖b‖

theorem dist_le_norm_add_norm {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b ≤ ‖a‖ + ‖b‖

theorem abs_norm_sub_norm_le_norm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

theorem abs_norm_sub_norm_le_norm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖-a + b‖

theorem norm_sub_norm_le_norm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a⁻¹ * b‖

theorem norm_sub_norm_le_norm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖-a + b‖

theorem norm_sub_le_norm_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a * b‖

theorem norm_sub_le_norm_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a + b‖

theorem dist_norm_norm_le_norm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a⁻¹ * b‖

theorem dist_norm_norm_le_norm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖-a + b‖

theorem norm_le_norm_add_norm_div' {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u - v‖

theorem norm_le_norm_add_norm_inv_mul {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖

theorem norm_le_norm_add_norm_neg_add {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖-u + v‖

theorem norm_le_norm_add_norm_div {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u - v‖

theorem norm_le_insert' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub'.

theorem norm_le_insert {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub.

theorem norm_le_mul_norm_add {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖u‖ ≤ ‖u * v‖ + ‖v‖

theorem norm_le_add_norm_add {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖u + v‖ + ‖v‖

theorem norm_le_mul_norm_add' {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖

An analogue of norm_le_mul_norm_add for the multiplication from the left.

theorem norm_le_add_norm_add' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u + v‖ + ‖u‖

An analogue of norm_le_add_norm_add for the addition from the left.

theorem norm_mul_eq_norm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x * y‖ = ‖y‖

theorem norm_add_eq_norm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x + y‖ = ‖y‖

theorem norm_mul_eq_norm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x * y‖ = ‖x‖

theorem norm_add_eq_norm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x + y‖ = ‖x‖

theorem norm_div_eq_norm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x / y‖ = ‖y‖

theorem norm_sub_eq_norm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x - y‖ = ‖y‖

theorem norm_div_eq_norm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x / y‖ = ‖x‖

theorem norm_sub_eq_norm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x - y‖ = ‖x‖

theorem ball_eq_norm_inv_mul_lt {E : Type u_5} [SeminormedGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖x⁻¹ * y‖ < ε}

theorem ball_eq_norm_neg_add_lt {E : Type u_5} [SeminormedAddGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖-x + y‖ < ε}

theorem ball_one_eq {E : Type u_5} [SeminormedGroup E] (r : ℝ) : Metric.ball 1 r = {x : E | ‖x‖ < r}

theorem ball_zero_eq {E : Type u_5} [SeminormedAddGroup E] (r : ℝ) : Metric.ball 0 r = {x : E | ‖x‖ < r}

theorem mem_ball_iff_norm_inv_mul_lt {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b⁻¹ * a‖ < r

theorem mem_ball_iff_norm_neg_add_lt {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖-b + a‖ < r

theorem mem_ball_iff_norm_inv_mul_lt' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a⁻¹ * b‖ < r

theorem mem_ball_iff_norm_neg_add_lt' {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖-a + b‖ < r

theorem mem_ball_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 1 r ↔ ‖a‖ < r

theorem mem_ball_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 0 r ↔ ‖a‖ < r

theorem mem_closedBall_iff_norm_inv_mul_le {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b⁻¹ * a‖ ≤ r

theorem mem_closedBall_iff_norm_neg_add_le {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖-b + a‖ ≤ r

theorem mem_closedBall_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_iff_norm_inv_mul_le' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r

theorem mem_closedBall_iff_norm_neg_add_le' {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖-a + b‖ ≤ r

theorem norm_le_of_mem_closedBall' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r

theorem norm_le_of_mem_closedBall {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r

theorem norm_le_norm_add_const_of_dist_le' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

theorem norm_le_norm_add_const_of_dist_le {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

theorem norm_lt_of_mem_ball' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r

theorem norm_lt_of_mem_ball {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r

theorem norm_div_sub_norm_div_le_norm_div {E : Type u_5} [SeminormedGroup E] (u v w : E) : ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_5} [SeminormedAddGroup E] (u v w : E) : ‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖

theorem norm_mul_sub_norm_div_le_two_mul {E : Type u_8} [SeminormedGroup E] (u v : E) : ‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

theorem norm_add_sub_norm_sub_le_two_mul {E : Type u_8} [SeminormedAddGroup E] (u v : E) : ‖u + v‖ - ‖u - v‖ ≤ 2 * ‖v‖

theorem norm_mul_sub_norm_div_le_two_mul_min {E : Type u_8} [SeminormedCommGroup E] (u v : E) : ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

theorem norm_add_sub_norm_sub_le_two_mul_min {E : Type u_8} [SeminormedAddCommGroup E] (u v : E) : ‖u + v‖ - ‖u - v‖ ≤ 2 * min ‖u‖ ‖v‖

theorem mem_sphere_iff_norm_inv_mul_eq {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b⁻¹ * a‖ = r

theorem mem_sphere_iff_norm_neg_add_eq {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖-b + a‖ = r

theorem mem_sphere_one_iff_norm {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 1 r ↔ ‖a‖ = r

theorem mem_sphere_zero_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 0 r ↔ ‖a‖ = r

@[simp]

theorem norm_eq_of_mem_sphere' {E : Type u_5} [SeminormedGroup E] {r : ℝ} (x : ↑(Metric.sphere 1 r)) : ‖↑x‖ = r

@[simp]

theorem norm_eq_of_mem_sphere {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (x : ↑(Metric.sphere 0 r)) : ‖↑x‖ = r

theorem ne_one_of_mem_sphere {E : Type u_5} [SeminormedGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 1 r)) : ↑x ≠ 1

theorem ne_zero_of_mem_sphere {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 0 r)) : ↑x ≠ 0

theorem ne_one_of_mem_unit_sphere {E : Type u_5} [SeminormedGroup E] (x : ↑(Metric.sphere 1 1)) : ↑x ≠ 1

theorem ne_zero_of_mem_unit_sphere {E : Type u_5} [SeminormedAddGroup E] (x : ↑(Metric.sphere 0 1)) : ↑x ≠ 0

def normGroupSeminorm (E : Type u_5) [SeminormedGroup E] : GroupSeminorm E

The norm of a seminormed group as a group seminorm.

def normAddGroupSeminorm (E : Type u_5) [SeminormedAddGroup E] : AddGroupSeminorm E

The norm of a seminormed group as an additive group seminorm.

@[simp]

theorem coe_normGroupSeminorm (E : Type u_5) [SeminormedGroup E] : ⇑(normGroupSeminorm E) = norm

@[simp]

theorem coe_normAddGroupSeminorm (E : Type u_5) [SeminormedAddGroup E] : ⇑(normAddGroupSeminorm E) = norm

theorem NormedGroup.tendsto_nhds_one {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

theorem NormedAddGroup.tendsto_nhds_zero {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

@[deprecated NormedGroup.tendsto_nhds_one (since := "2026-02-17")]

theorem NormedCommGroup.tendsto_nhds_one {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

Alias of NormedGroup.tendsto_nhds_one.

@[deprecated NormedAddGroup.tendsto_nhds_zero (since := "2026-02-17")]

theorem NormedAddCommGroup.tendsto_nhds_zero {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

Alias of NormedAddGroup.tendsto_nhds_zero.

theorem NormedGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x'⁻¹ * x‖ < δ → ‖(f x')⁻¹ * y‖ < ε

theorem NormedAddGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖-x' + x‖ < δ → ‖-f x' + y‖ < ε

theorem NormedGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y⁻¹ * x‖ < ε}

theorem NormedAddGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedAddGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖-y + x‖ < ε}

theorem NormedGroup.nhds_one_basis_norm_lt {E : Type u_5} [SeminormedGroup E] : (nhds 1).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

theorem NormedAddGroup.nhds_zero_basis_norm_lt {E : Type u_5} [SeminormedAddGroup E] : (nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

@[deprecated NormedGroup.nhds_one_basis_norm_lt (since := "2026-02-17")]

theorem NormedCommGroup.nhds_one_basis_norm_lt {E : Type u_5} [SeminormedGroup E] : (nhds 1).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

Alias of NormedGroup.nhds_one_basis_norm_lt.

@[deprecated NormedAddGroup.nhds_zero_basis_norm_lt (since := "2026-02-17")]

theorem NormedAddCommGroup.nhds_zero_basis_norm_lt {E : Type u_5} [SeminormedAddGroup E] : (nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

Alias of NormedAddGroup.nhds_zero_basis_norm_lt.

theorem NormedGroup.uniformity_basis_dist {E : Type u_5} [SeminormedGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}

theorem NormedAddGroup.uniformity_basis_dist {E : Type u_5} [SeminormedAddGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖-p.1 + p.2‖ < ε}

@[implicit_reducible, instance 100]

instance SeminormedGroup.toNNNorm {E : Type u_5} [SeminormedGroup E] : NNNorm E

@[implicit_reducible, instance 100]

instance SeminormedAddGroup.toNNNorm {E : Type u_5} [SeminormedAddGroup E] : NNNorm E

@[simp]

theorem coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (a : E) : ↑‖a‖₊ = ‖a‖

@[simp]

theorem coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : ↑‖a‖₊ = ‖a‖

@[simp]

theorem coe_comp_nnnorm' {E : Type u_5} [SeminormedGroup E] : NNReal.toReal ∘ nnnorm = norm

@[simp]

theorem coe_comp_nnnorm {E : Type u_5} [SeminormedAddGroup E] : NNReal.toReal ∘ nnnorm = norm

@[simp]

theorem norm_toNNReal' {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖.toNNReal = ‖a‖₊

@[simp]

theorem norm_toNNReal {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖.toNNReal = ‖a‖₊

@[simp]

theorem toReal_enorm' {E : Type u_5} [SeminormedGroup E] (x : E) : ‖x‖ₑ.toReal = ‖x‖

@[simp]

theorem toReal_enorm {E : Type u_5} [SeminormedAddGroup E] (x : E) : ‖x‖ₑ.toReal = ‖x‖

@[simp]

theorem ofReal_norm' {E : Type u_5} [SeminormedGroup E] (x : E) : ENNReal.ofReal ‖x‖ = ‖x‖ₑ

@[simp]

theorem ofReal_norm {E : Type u_5} [SeminormedAddGroup E] (x : E) : ENNReal.ofReal ‖x‖ = ‖x‖ₑ

theorem enorm'_eq_iff_norm_eq {E : Type u_5} {F : Type u_6} [SeminormedGroup E] [SeminormedGroup F] {x : E} {y : F} : ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

theorem enorm_eq_iff_norm_eq {E : Type u_5} {F : Type u_6} [SeminormedAddGroup E] [SeminormedAddGroup F] {x : E} {y : F} : ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

theorem enorm'_le_iff_norm_le {E : Type u_5} {F : Type u_6} [SeminormedGroup E] [SeminormedGroup F] {x : E} {y : F} : ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

theorem enorm_le_iff_norm_le {E : Type u_5} {F : Type u_6} [SeminormedAddGroup E] [SeminormedAddGroup F] {x : E} {y : F} : ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

theorem nndist_eq_nnnorm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : nndist a b = ‖a⁻¹ * b‖₊

theorem nndist_eq_nnnorm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : nndist a b = ‖-a + b‖₊

@[simp]

theorem nnnorm_inv' {E : Type u_5} [SeminormedGroup E] (a : E) : ‖a⁻¹‖₊ = ‖a‖₊

@[simp]

theorem nnnorm_neg {E : Type u_5} [SeminormedAddGroup E] (a : E) : ‖-a‖₊ = ‖a‖₊

@[simp]

theorem nndist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : nndist a 1 = ‖a‖₊

@[simp]

theorem nndist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : nndist a 0 = ‖a‖₊

@[simp]

theorem edist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : edist a 1 = ‖a‖ₑ

@[simp]

theorem edist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : edist a 0 = ‖a‖ₑ

@[simp]

theorem nnnorm_one' {E : Type u_5} [SeminormedGroup E] : ‖1‖₊ = 0

@[simp]

theorem nnnorm_zero {E : Type u_5} [SeminormedAddGroup E] : ‖0‖₊ = 0

theorem ne_one_of_nnnorm_ne_zero {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖₊ ≠ 0 → a ≠ 1

theorem ne_zero_of_nnnorm_ne_zero {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖₊ ≠ 0 → a ≠ 0

theorem nnnorm_mul_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnnorm_add_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem norm_pow_le_mul_norm {E : Type u_5} [SeminormedGroup E] {a : E} {n : ℕ} : ‖a ^ n‖ ≤ ↑n * ‖a‖

theorem norm_nsmul_le {E : Type u_5} [SeminormedAddGroup E] {a : E} {n : ℕ} : ‖n • a‖ ≤ ↑n * ‖a‖

theorem nnnorm_pow_le_mul_norm {E : Type u_5} [SeminormedGroup E] {a : E} {n : ℕ} : ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

theorem nnnorm_nsmul_le {E : Type u_5} [SeminormedAddGroup E] {a : E} {n : ℕ} : ‖n • a‖₊ ≤ ↑n * ‖a‖₊

@[simp]

theorem nnnorm_zpow_abs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ |n|‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnnorm_abs_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖|n| • a‖₊ = ‖n • a‖₊

@[simp]

theorem nnnorm_pow_natAbs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnnorm_natAbs_smul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖n.natAbs • a‖₊ = ‖n • a‖₊

theorem nnnorm_zpow_isUnit {E : Type u_5} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖₊ = ‖a‖₊

theorem nnnorm_isUnit_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖n • a‖₊ = ‖a‖₊

@[simp]

theorem nnnorm_units_zsmul {E : Type u_8} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖₊ = ‖a‖₊

@[simp]

theorem nndist_one_left {E : Type u_5} [SeminormedGroup E] (a : E) : nndist 1 a = ‖a‖₊

@[simp]

theorem nndist_zero_left {E : Type u_5} [SeminormedAddGroup E] (a : E) : nndist 0 a = ‖a‖₊

@[simp]

theorem edist_one_left {E : Type u_5} [SeminormedGroup E] (a : E) : edist 1 a = ↑‖a‖₊

@[simp]

theorem edist_zero_left {E : Type u_5} [SeminormedAddGroup E] (a : E) : edist 0 a = ↑‖a‖₊

theorem nndist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖₊

theorem nndist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : nndist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖₊

theorem nnnorm_div_le {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnnorm_sub_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem enorm_div_le {E : Type u_5} [SeminormedGroup E] {a b : E} : ‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_sub_le {E : Type u_5} [SeminormedAddGroup E] {a b : E} : ‖a - b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem nndist_nnnorm_nnnorm_le_nnnorm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a⁻¹ * b‖₊

theorem nndist_nnnorm_nnnorm_le_nnnorm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖-a + b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_div {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_sub {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_div' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_sub' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊

theorem nnnorm_le_insert' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

theorem nnnorm_le_insert {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub.

theorem nnnorm_le_mul_nnnorm_add {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

theorem nnnorm_le_add_nnnorm_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊

theorem nnnorm_le_mul_nnnorm_add' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊

An analogue of nnnorm_le_mul_nnnorm_add for the multiplication from the left.

theorem nnnorm_le_add_nnnorm_add' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a + b‖₊ + ‖a‖₊

An analogue of nnnorm_le_add_nnnorm_add for the addition from the left.

theorem nnnorm_mul_eq_nnnorm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x * y‖₊ = ‖y‖₊

theorem nnnorm_add_eq_nnnorm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x + y‖₊ = ‖y‖₊

theorem nnnorm_mul_eq_nnnorm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x * y‖₊ = ‖x‖₊

theorem nnnorm_add_eq_nnnorm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x + y‖₊ = ‖x‖₊

theorem nnnorm_div_eq_nnnorm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x / y‖₊ = ‖y‖₊

theorem nnnorm_sub_eq_nnnorm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x - y‖₊ = ‖y‖₊

theorem nnnorm_div_eq_nnnorm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x / y‖₊ = ‖x‖₊

theorem nnnorm_sub_eq_nnnorm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x - y‖₊ = ‖x‖₊

theorem toReal_coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (a : E) : (↑‖a‖₊).toReal = ‖a‖

The nonnegative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem toReal_coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : (↑‖a‖₊).toReal = ‖a‖

The nonnegative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem edist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(symmDiff s t).mulIndicator f x‖₊

theorem edist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : edist (s.indicator f x) (t.indicator f x) = ↑‖(symmDiff s t).indicator f x‖₊

theorem nontrivialTopology_iff_exists_nnnorm_ne_zero' {E : Type u_5} [SeminormedGroup E] : NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

theorem nontrivialTopology_iff_exists_nnnorm_ne_zero {E : Type u_5} [SeminormedAddGroup E] : NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

theorem indiscreteTopology_iff_forall_nnnorm_eq_zero' {E : Type u_5} [SeminormedGroup E] : IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

theorem indiscreteTopology_iff_forall_nnnorm_eq_zero {E : Type u_5} [SeminormedAddGroup E] : IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

theorem exists_nnnorm_ne_zero' (E : Type u_5) [SeminormedGroup E] [NontrivialTopology E] : ∃ (x : E), ‖x‖₊ ≠ 0

theorem exists_nnnorm_ne_zero (E : Type u_5) [SeminormedAddGroup E] [NontrivialTopology E] : ∃ (x : E), ‖x‖₊ ≠ 0

theorem IndiscreteTopology.nnnorm_eq_zero' {E : Type u_5} [SeminormedGroup E] [IndiscreteTopology E] (x : E) : ‖x‖₊ = 0

theorem IndiscreteTopology.nnnorm_eq_zero {E : Type u_5} [SeminormedAddGroup E] [IndiscreteTopology E] (x : E) : ‖x‖₊ = 0

theorem NontrivialTopology.of_exists_nnnorm_ne_zero' {E : Type u_5} [SeminormedGroup E] : (∃ (x : E), ‖x‖₊ ≠ 0) → NontrivialTopology E

Alias of the reverse direction of nontrivialTopology_iff_exists_nnnorm_ne_zero'.

theorem NontrivialTopology.of_exists_nnnorm_ne_zero {E : Type u_5} [SeminormedAddGroup E] : (∃ (x : E), ‖x‖₊ ≠ 0) → NontrivialTopology E

Alias of the reverse direction of nontrivialTopology_iff_exists_nnnorm_ne_zero.

theorem IndiscreteTopology.of_forall_nnnorm_eq_zero' {E : Type u_5} [SeminormedGroup E] : (∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E

Alias of the reverse direction of indiscreteTopology_iff_forall_nnnorm_eq_zero'.

theorem IndiscreteTopology.of_forall_nnnorm_eq_zero {E : Type u_5} [SeminormedAddGroup E] : (∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E

Alias of the reverse direction of indiscreteTopology_iff_forall_nnnorm_eq_zero.

theorem nontrivialTopology_iff_exists_norm_ne_zero' {E : Type u_5} [SeminormedGroup E] : NontrivialTopology E ↔ ∃ (x : E), ‖x‖ ≠ 0

theorem nontrivialTopology_iff_exists_norm_ne_zero {E : Type u_5} [SeminormedAddGroup E] : NontrivialTopology E ↔ ∃ (x : E), ‖x‖ ≠ 0

theorem indiscreteTopology_iff_forall_norm_eq_zero' {E : Type u_5} [SeminormedGroup E] : IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

theorem indiscreteTopology_iff_forall_norm_eq_zero {E : Type u_5} [SeminormedAddGroup E] : IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

theorem exists_norm_ne_zero' (E : Type u_5) [SeminormedGroup E] [NontrivialTopology E] : ∃ (x : E), ‖x‖ ≠ 0

theorem exists_norm_ne_zero (E : Type u_5) [SeminormedAddGroup E] [NontrivialTopology E] : ∃ (x : E), ‖x‖ ≠ 0

theorem IndiscreteTopology.norm_eq_zero' {E : Type u_5} [SeminormedGroup E] [IndiscreteTopology E] (x : E) : ‖x‖ = 0

theorem IndiscreteTopology.norm_eq_zero {E : Type u_5} [SeminormedAddGroup E] [IndiscreteTopology E] (x : E) : ‖x‖ = 0

theorem NontrivialTopology.of_exists_norm_ne_zero' {E : Type u_5} [SeminormedGroup E] : (∃ (x : E), ‖x‖ ≠ 0) → NontrivialTopology E

Alias of the reverse direction of nontrivialTopology_iff_exists_norm_ne_zero'.

theorem NontrivialTopology.of_exists_norm_ne_zero {E : Type u_5} [SeminormedAddGroup E] : (∃ (x : E), ‖x‖ ≠ 0) → NontrivialTopology E

Alias of the reverse direction of nontrivialTopology_iff_exists_norm_ne_zero.

theorem IndiscreteTopology.of_forall_norm_eq_zero' {E : Type u_5} [SeminormedGroup E] : (∀ (x : E), ‖x‖ = 0) → IndiscreteTopology E

Alias of the reverse direction of indiscreteTopology_iff_forall_norm_eq_zero'.

theorem IndiscreteTopology.of_forall_norm_eq_zero {E : Type u_5} [SeminormedAddGroup E] : (∀ (x : E), ‖x‖ = 0) → IndiscreteTopology E

Alias of the reverse direction of indiscreteTopology_iff_forall_norm_eq_zero.

@[simp]

theorem enorm_one' {E : Type u_8} [TopologicalSpace E] [ESeminormedMonoid E] : ‖1‖ₑ = 0

@[simp]

theorem enorm_zero {E : Type u_8} [TopologicalSpace E] [ESeminormedAddMonoid E] : ‖0‖ₑ = 0

theorem exists_enorm_lt' (E : Type u_8) [TopologicalSpace E] [ESeminormedMonoid E] [hbot : (nhdsWithin 1 {1}ᶜ).NeBot] {c : ENNReal} (hc : c ≠ 0) : ∃ (x : E), x ≠ 1 ∧ ‖x‖ₑ < c

theorem exists_enorm_lt (E : Type u_8) [TopologicalSpace E] [ESeminormedAddMonoid E] [hbot : (nhdsWithin 0 {0}ᶜ).NeBot] {c : ENNReal} (hc : c ≠ 0) : ∃ (x : E), x ≠ 0 ∧ ‖x‖ₑ < c

@[simp]

theorem enorm_inv' {E : Type u_5} [SeminormedGroup E] (a : E) : ‖a⁻¹‖ₑ = ‖a‖ₑ

@[simp]

theorem enorm_neg {E : Type u_5} [SeminormedAddGroup E] (a : E) : ‖-a‖ₑ = ‖a‖ₑ

theorem ofReal_norm_eq_enorm' {E : Type u_5} [SeminormedGroup E] (a : E) : ENNReal.ofReal ‖a‖ = ‖a‖ₑ

theorem ofReal_norm_eq_enorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : ENNReal.ofReal ‖a‖ = ‖a‖ₑ

theorem edist_eq_enorm_inv_mul {E : Type u_5} [SeminormedGroup E] (a b : E) : edist a b = ‖a⁻¹ * b‖ₑ

theorem edist_eq_enorm_neg_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : edist a b = ‖-a + b‖ₑ

@[deprecated edist_one_right (since := "2026-02-11")]

theorem edist_one_eq_enorm {E : Type u_5} [SeminormedGroup E] (a : E) : edist a 1 = ‖a‖ₑ

Alias of edist_one_right.

@[deprecated edist_zero_right (since := "2026-02-11")]

theorem edist_zero_eq_enorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : edist a 0 = ‖a‖ₑ

Alias of edist_zero_right.

theorem enorm_div_rev {E : Type u_8} [SeminormedGroup E] (a b : E) : ‖a / b‖ₑ = ‖b / a‖ₑ

theorem enorm_sub_rev {E : Type u_8} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ₑ = ‖b - a‖ₑ

theorem mem_eball_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r

theorem mem_eball_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r

@[deprecated mem_eball_zero_iff (since := "2026-01-24")]

theorem mem_emetric_ball_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r

Alias of mem_eball_zero_iff.

@[deprecated mem_eball_one_iff (since := "2026-01-24")]

theorem mem_emetric_ball_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ENNReal} : a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r

Alias of mem_eball_one_iff.

theorem enorm_mul_le' {E : Type u_8} [TopologicalSpace E] [ESeminormedMonoid E] (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_add_le {E : Type u_8} [TopologicalSpace E] [ESeminormedAddMonoid E] (a b : E) : ‖a + b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_mul_le_of_le' {E : Type u_8} [TopologicalSpace E] [ESeminormedMonoid E] {r₁ r₂ : ENNReal} {a₁ a₂ : E} (h₁ : ‖a₁‖ₑ ≤ r₁) (h₂ : ‖a₂‖ₑ ≤ r₂) : ‖a₁ * a₂‖ₑ ≤ r₁ + r₂

theorem enorm_add_le_of_le {E : Type u_8} [TopologicalSpace E] [ESeminormedAddMonoid E] {r₁ r₂ : ENNReal} {a₁ a₂ : E} (h₁ : ‖a₁‖ₑ ≤ r₁) (h₂ : ‖a₂‖ₑ ≤ r₂) : ‖a₁ + a₂‖ₑ ≤ r₁ + r₂

theorem enorm_mul₃_le' {E : Type u_8} [TopologicalSpace E] [ESeminormedMonoid E] {a b c : E} : ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ

theorem enorm_add₃_le {E : Type u_8} [TopologicalSpace E] [ESeminormedAddMonoid E] {a b c : E} : ‖a + b + c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ

theorem enorm_mul₄_le' {E : Type u_8} [TopologicalSpace E] [ESeminormedMonoid E] {a b c d : E} : ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ

theorem enorm_add₄_le {E : Type u_8} [TopologicalSpace E] [ESeminormedAddMonoid E] {a b c d : E} : ‖a + b + c + d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ

@[simp]

theorem enorm_eq_zero' {E : Type u_8} [TopologicalSpace E] [ENormedMonoid E] {a : E} : ‖a‖ₑ = 0 ↔ a = 1

@[simp]

theorem enorm_eq_zero {E : Type u_8} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} : ‖a‖ₑ = 0 ↔ a = 0

theorem enorm_ne_zero' {E : Type u_8} [TopologicalSpace E] [ENormedMonoid E] {a : E} : ‖a‖ₑ ≠ 0 ↔ a ≠ 1

theorem enorm_ne_zero {E : Type u_8} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} : ‖a‖ₑ ≠ 0 ↔ a ≠ 0

@[simp]

theorem enorm_pos' {E : Type u_8} [TopologicalSpace E] [ENormedMonoid E] {a : E} : 0 < ‖a‖ₑ ↔ a ≠ 1

@[simp]

theorem enorm_pos {E : Type u_8} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} : 0 < ‖a‖ₑ ↔ a ≠ 0

theorem SeminormedGroup.disjoint_nhds {E : Type u_5} [SeminormedGroup E] (x : E) (f : Filter E) : Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y⁻¹ * x‖

theorem SeminormedAddGroup.disjoint_nhds {E : Type u_5} [SeminormedAddGroup E] (x : E) (f : Filter E) : Disjoint (nhds x) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖-y + x‖

theorem SeminormedGroup.disjoint_nhds_one {E : Type u_5} [SeminormedGroup E] (f : Filter E) : Disjoint (nhds 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

theorem SeminormedAddGroup.disjoint_nhds_zero {E : Type u_5} [SeminormedAddGroup E] (f : Filter E) : Disjoint (nhds 0) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

@[reducible, inline]

abbrev SeminormedGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedGroup E

A group homomorphism from a Group to a SeminormedGroup induces a SeminormedGroup structure on the domain.

@[reducible, inline]

abbrev SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedAddGroup E

A group homomorphism from an AddGroup to a SeminormedAddGroup induces a SeminormedAddGroup structure on the domain.

@[reducible, inline]

abbrev SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedCommGroup E

A group homomorphism from a CommGroup to a SeminormedGroup induces a SeminormedCommGroup structure on the domain.

@[reducible, inline]

abbrev SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddCommGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedAddCommGroup E

A group homomorphism from an AddCommGroup to a SeminormedAddGroup induces a SeminormedAddCommGroup structure on the domain.

@[reducible, inline]

abbrev NormedGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedGroup E

An injective group homomorphism from a Group to a NormedGroup induces a NormedGroup structure on the domain.

@[reducible, inline]

abbrev NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedAddGroup E

An injective group homomorphism from an AddGroup to a NormedAddGroup induces a NormedAddGroup structure on the domain.

@[reducible, inline]

abbrev NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedCommGroup E

An injective group homomorphism from a CommGroup to a NormedGroup induces a NormedCommGroup structure on the domain.

@[reducible, inline]

abbrev NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddCommGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedAddCommGroup E

An injective group homomorphism from a CommGroup to a NormedCommGroup induces a NormedCommGroup structure on the domain.

theorem dist_eq_norm_div {E : Type u_5} [SeminormedCommGroup E] (a b : E) : dist a b = ‖a / b‖

theorem dist_eq_norm_sub {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : dist a b = ‖a - b‖

theorem dist_eq_norm_div' {E : Type u_5} [SeminormedCommGroup E] (a b : E) : dist a b = ‖b / a‖

theorem dist_eq_norm_sub' {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : dist a b = ‖b - a‖

theorem dist_eq_norm {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : dist a b = ‖a - b‖

Alias of dist_eq_norm_sub.

theorem dist_eq_norm' {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : dist a b = ‖b - a‖

Alias of dist_eq_norm_sub'.

theorem norm_inv_mul {E : Type u_5} [SeminormedCommGroup E] (a b : E) : ‖a⁻¹ * b‖ = ‖a / b‖

theorem norm_neg_add {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : ‖-a + b‖ = ‖a - b‖

theorem abs_norm_sub_norm_le' {E : Type u_5} [SeminormedCommGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a / b‖

theorem abs_norm_sub_norm_le {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a - b‖

theorem norm_sub_norm_le' {E : Type u_5} [SeminormedCommGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a / b‖

theorem norm_sub_norm_le {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a - b‖

theorem dist_norm_norm_le' {E : Type u_5} [SeminormedCommGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a / b‖

theorem dist_norm_norm_le {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a - b‖

theorem nndist_nnnorm_nnnorm_le' {E : Type u_5} [SeminormedCommGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

theorem nndist_nnnorm_nnnorm_le {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊

theorem nndist_eq_nnnorm_div {E : Type u_5} [SeminormedCommGroup E] (a b : E) : nndist a b = ‖a / b‖₊

theorem nndist_eq_nnnorm_sub {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : nndist a b = ‖a - b‖₊

theorem nndist_eq_nnnorm {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : nndist a b = ‖a - b‖₊

Alias of nndist_eq_nnnorm_sub.

theorem edist_eq_enorm_div {E : Type u_5} [SeminormedCommGroup E] (a b : E) : edist a b = ‖a / b‖ₑ

theorem edist_eq_enorm_sub {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) : edist a b = ‖a - b‖ₑ

theorem dist_inv {E : Type u_5} [SeminormedCommGroup E] (x y : E) : dist x⁻¹ y = dist x y⁻¹

theorem dist_neg {E : Type u_5} [SeminormedAddCommGroup E] (x y : E) : dist (-x) y = dist x (-y)

theorem norm_multiset_sum_le {E : Type u_9} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem enorm_multisetSum_le {ε : Type u_9} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] (m : Multiset ε) : ‖m.sum‖ₑ ≤ (Multiset.map (fun (x : ε) => ‖x‖ₑ) m).sum

theorem norm_multiset_prod_le {E : Type u_5} [SeminormedCommGroup E] (m : Multiset E) : ‖m.prod‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem enorm_multisetProd_le {ε : Type u_9} [TopologicalSpace ε] [ESeminormedCommMonoid ε] (m : Multiset ε) : ‖m.prod‖ₑ ≤ (Multiset.map (fun (x : ε) => ‖x‖ₑ) m).sum

theorem enorm_sum_le {ι : Type u_3} {ε : Type u_9} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] (s : Finset ι) (f : ι → ε) : ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem norm_sum_le {ι : Type u_3} {E : Type u_9} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

theorem enorm_prod_le {ι : Type u_3} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedCommMonoid ε] (s : Finset ι) (f : ι → ε) : ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem norm_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

theorem enorm_prod_le_of_le {ι : Type u_3} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedCommMonoid ε] (s : Finset ι) {f : ι → ε} {n : ι → ENNReal} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) : ‖∏ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b

theorem enorm_sum_le_of_le {ι : Type u_3} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] (s : Finset ι) {f : ι → ε} {n : ι → ENNReal} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) : ‖∑ b ∈ s, f b‖ₑ ≤ ∑ b ∈ s, n b

theorem norm_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖∏ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b

theorem norm_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖∑ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b

theorem dist_prod_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

theorem dist_sum_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, d b

theorem dist_prod_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f a : ι → E) : dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

theorem dist_sum_sum_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) (f a : ι → E) : dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

theorem ball_eq' {E : Type u_5} [SeminormedCommGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖x / y‖ < ε}

theorem ball_eq {E : Type u_5} [SeminormedAddCommGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖x - y‖ < ε}

theorem mem_ball_iff_norm'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b / a‖ < r

theorem mem_ball_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b - a‖ < r

theorem mem_ball_iff_norm''' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a / b‖ < r

theorem mem_ball_iff_norm' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a - b‖ < r

theorem mem_closedBall_iff_norm'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r

theorem mem_closedBall_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r

theorem mem_closedBall_iff_norm''' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r

theorem mem_closedBall_iff_norm' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r

@[simp]

theorem mem_sphere_iff_norm' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b / a‖ = r

@[simp]

theorem mem_sphere_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b - a‖ = r

theorem mul_mem_ball_iff_norm {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem add_mem_ball_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem mul_mem_closedBall_iff_norm {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

theorem add_mem_closedBall_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

@[simp]

theorem preimage_mul_ball {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r

@[simp]

theorem preimage_add_ball {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r

@[simp]

theorem preimage_mul_closedBall {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r

@[simp]

theorem preimage_add_closedBall {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r

@[simp]

theorem preimage_mul_sphere {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r

@[simp]

theorem preimage_add_sphere {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r

theorem pow_mem_closedBall {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : a ^ n ∈ Metric.closedBall (b ^ n) (n • r)

theorem nsmul_mem_closedBall {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : n • a ∈ Metric.closedBall (n • b) (n • r)

theorem pow_mem_ball {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : a ^ n ∈ Metric.ball (b ^ n) (n • r)

theorem nsmul_mem_ball {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : n • a ∈ Metric.ball (n • b) (n • r)

theorem mul_mem_closedBall_mul_iff {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.closedBall (b * c) r ↔ a ∈ Metric.closedBall b r

theorem add_mem_closedBall_add_iff {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.closedBall (b + c) r ↔ a ∈ Metric.closedBall b r

theorem mul_mem_ball_mul_iff {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.ball (b * c) r ↔ a ∈ Metric.ball b r

theorem add_mem_ball_add_iff {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.ball (b + c) r ↔ a ∈ Metric.ball b r

theorem smul_closedBall'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.closedBall b r = Metric.closedBall (a • b) r

theorem vadd_closedBall'' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r

theorem smul_ball'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.ball b r = Metric.ball (a • b) r

theorem vadd_ball'' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r

theorem nnnorm_multiset_prod_le {E : Type u_5} [SeminormedCommGroup E] (m : Multiset E) : ‖m.prod‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

theorem nnnorm_multiset_sum_le {E : Type u_5} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

theorem nnnorm_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

theorem nnnorm_sum_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

theorem nnnorm_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

theorem nnnorm_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

theorem NormedCommGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedCommGroup E] [SeminormedCommGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

theorem NormedAddCommGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' - x‖ < δ → ‖f x' - y‖ < ε

theorem NormedCommGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedCommGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y / x‖ < ε}

theorem NormedAddCommGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedAddCommGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y - x‖ < ε}

theorem NormedCommGroup.uniformity_basis_dist {E : Type u_5} [SeminormedCommGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 / p.2‖ < ε}

theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_5} [SeminormedAddCommGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 - p.2‖ < ε}

@[simp]

theorem norm_le_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1

@[simp]

theorem norm_le_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 0

@[simp]

theorem norm_pos_iff' {E : Type u_5} [NormedGroup E] {a : E} : 0 < ‖a‖ ↔ a ≠ 1

@[simp]

theorem norm_pos_iff {E : Type u_5} [NormedAddGroup E] {a : E} : 0 < ‖a‖ ↔ a ≠ 0

@[simp]

theorem norm_eq_zero' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ = 0 ↔ a = 1

@[simp]

theorem norm_eq_zero {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ = 0 ↔ a = 0

theorem norm_ne_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≠ 0 ↔ a ≠ 1

theorem norm_ne_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ ≠ 0 ↔ a ≠ 0

theorem norm_div_eq_zero_iff {E : Type u_5} [NormedGroup E] {a b : E} : ‖a / b‖ = 0 ↔ a = b

theorem norm_sub_eq_zero_iff {E : Type u_5} [NormedAddGroup E] {a b : E} : ‖a - b‖ = 0 ↔ a = b

theorem norm_div_pos_iff {E : Type u_5} [NormedGroup E] {a b : E} : 0 < ‖a / b‖ ↔ a ≠ b

theorem norm_sub_pos_iff {E : Type u_5} [NormedAddGroup E] {a b : E} : 0 < ‖a - b‖ ↔ a ≠ b

theorem eq_of_norm_div_le_zero {E : Type u_5} [NormedGroup E] {a b : E} (h : ‖a / b‖ ≤ 0) : a = b

theorem eq_of_norm_sub_le_zero {E : Type u_5} [NormedAddGroup E] {a b : E} (h : ‖a - b‖ ≤ 0) : a = b

theorem eq_of_norm_div_eq_zero {E : Type u_5} [NormedGroup E] {a b : E} : ‖a / b‖ = 0 → a = b

Alias of the forward direction of norm_div_eq_zero_iff.

theorem eq_of_norm_sub_eq_zero {E : Type u_5} [NormedAddGroup E] {a b : E} : ‖a - b‖ = 0 → a = b

theorem eq_one_or_norm_pos {E : Type u_5} [NormedGroup E] (a : E) : a = 1 ∨ 0 < ‖a‖

theorem eq_zero_or_norm_pos {E : Type u_5} [NormedAddGroup E] (a : E) : a = 0 ∨ 0 < ‖a‖

theorem eq_one_or_nnnorm_pos {E : Type u_5} [NormedGroup E] (a : E) : a = 1 ∨ 0 < ‖a‖₊

theorem eq_zero_or_nnnorm_pos {E : Type u_5} [NormedAddGroup E] (a : E) : a = 0 ∨ 0 < ‖a‖₊

@[simp]

theorem nnnorm_eq_zero' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖₊ = 0 ↔ a = 1

@[simp]

theorem nnnorm_eq_zero {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖₊ = 0 ↔ a = 0

theorem nnnorm_ne_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖₊ ≠ 0 ↔ a ≠ 1

theorem nnnorm_ne_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖₊ ≠ 0 ↔ a ≠ 0

@[simp]

theorem nnnorm_pos' {E : Type u_5} [NormedGroup E] {a : E} : 0 < ‖a‖₊ ↔ a ≠ 1

@[simp]

theorem nnnorm_pos {E : Type u_5} [NormedAddGroup E] {a : E} : 0 < ‖a‖₊ ↔ a ≠ 0

def normGroupNorm (E : Type u_5) [NormedGroup E] : GroupNorm E

The norm of a normed group as a group norm.

def normAddGroupNorm (E : Type u_5) [NormedAddGroup E] : AddGroupNorm E

The norm of a normed group as an additive group norm.

@[simp]

theorem coe_normGroupNorm (E : Type u_5) [NormedGroup E] : ⇑(normGroupNorm E) = norm

Some relations with HasCompactSupport

theorem hasCompactSupport_norm_iff {α : Type u_2} {E : Type u_5} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : (HasCompactSupport fun (x : α) => ‖f x‖) ↔ HasCompactSupport f

theorem HasCompactSupport.norm {α : Type u_2} {E : Type u_5} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : HasCompactSupport f → HasCompactSupport fun (x : α) => ‖f x‖

Alias of the reverse direction of hasCompactSupport_norm_iff.

positivity extensions

def Mathlib.Meta.Positivity.evalMulNorm : PositivityExt

Extension for the positivity tactic: multiplicative norms are always nonnegative, and positive on non-one inputs.

def Mathlib.Meta.Positivity.evalAddNorm : PositivityExt

Extension for the positivity tactic: additive norms are always nonnegative, and positive on non-zero inputs.