Documentation

theorem dist_eq_norm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

dist a b = ‖a⁻¹ * b‖

theorem dist_eq_norm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

dist a b = ‖-a + b‖

theorem dist_eq_norm_inv_mul' {E : Type u_4} [SeminormedGroup E] (a b : E) :

dist a b = ‖b⁻¹ * a‖

theorem dist_eq_norm_neg_add' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

dist a b = ‖-b + a‖

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

DiscreteTopology E

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

DiscreteTopology E

@[simp]

theorem dist_one_right {E : Type u_4} [SeminormedGroup E] (a : E) :

dist a 1 = ‖a‖

@[simp]

theorem dist_zero_right {E : Type u_4} [SeminormedAddGroup E] (a : E) :

dist a 0 = ‖a‖

theorem inseparable_one_iff_norm {E : Type u_4} [SeminormedGroup E] {a : E} :

Inseparable a 1 ↔ ‖a‖ = 0

theorem inseparable_zero_iff_norm {E : Type u_4} [SeminormedAddGroup E] {a : E} :

Inseparable a 0 ↔ ‖a‖ = 0

theorem dist_one_left {E : Type u_4} [SeminormedGroup E] (a : E) :

dist 1 a = ‖a‖

theorem dist_zero_left {E : Type u_4} [SeminormedAddGroup E] (a : E) :

dist 0 a = ‖a‖

@[simp]

theorem dist_one {E : Type u_4} [SeminormedGroup E] :

dist 1 = norm

@[simp]

theorem dist_zero {E : Type u_4} [SeminormedAddGroup E] :

dist 0 = norm

theorem norm_div_rev {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a / b‖ = ‖b / a‖

theorem norm_sub_rev {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a - b‖ = ‖b - a‖

@[simp]

theorem norm_inv' {E : Type u_4} [SeminormedGroup E] (a : E) :

‖a⁻¹ ‖ = ‖a‖

@[simp]

theorem norm_neg {E : Type u_4} [SeminormedAddGroup E] (a : E) :

‖-a‖ = ‖a‖

@[simp]

theorem norm_zpow_abs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ |n|‖ = ‖a ^ n‖

@[simp]

theorem norm_abs_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖|n| • a‖ = ‖n • a‖

@[simp]

theorem norm_pow_natAbs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ n.natAbs‖ = ‖a ^ n‖

@[simp]

theorem norm_natAbs_smul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖n.natAbs • a‖ = ‖n • a‖

theorem norm_zpow_isUnit {E : Type u_4} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

‖a ^ n‖ = ‖a‖

theorem norm_isUnit_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

‖n • a‖ = ‖a‖

@[simp]

theorem norm_units_zsmul {E : Type u_7} [SeminormedAddGroup E] (n : ℤ ˣ) (a : E) :

‖n • a‖ = ‖a‖

theorem dist_mulIndicator {α : Type u_2} {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] (a b : E) :

‖a * b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_add_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a + b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_mul_le_of_le' {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] {a b c : E} :

‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_add₃_le {E : Type u_4} [SeminormedAddGroup E] {a b c : E} :

‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_mul₄_le' {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] (a b c : E) :

‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

theorem norm_sub_le_norm_sub_add_norm_sub {E : Type u_4} [SeminormedAddGroup E] (a b c : E) :

‖a - c‖ ≤ ‖a - b‖ + ‖b - c‖

theorem norm_le_norm_div_add {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖ ≤ ‖a / b‖ + ‖b‖

theorem norm_le_norm_sub_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a‖ ≤ ‖a - b‖ + ‖b‖

@[simp]

theorem norm_nonneg' {E : Type u_4} [SeminormedGroup E] (a : E) :

0 ≤ ‖a‖

@[simp]

theorem norm_nonneg {E : Type u_4} [SeminormedAddGroup E] (a : E) :

0 ≤ ‖a‖

@[simp]

theorem abs_norm' {E : Type u_4} [SeminormedGroup E] (z : E) :

|‖z‖| = ‖z‖

@[simp]

theorem abs_norm {E : Type u_4} [SeminormedAddGroup E] (z : E) :

|‖z‖| = ‖z‖

@[simp]

theorem norm_one' {E : Type u_4} [SeminormedGroup E] :

‖1‖ = 0

@[simp]

theorem norm_zero {E : Type u_4} [SeminormedAddGroup E] :

‖0‖ = 0

theorem ne_one_of_norm_ne_zero {E : Type u_4} [SeminormedGroup E] {a : E} :

‖a‖ ≠ 0 → a ≠ 1

theorem ne_zero_of_norm_ne_zero {E : Type u_4} [SeminormedAddGroup E] {a : E} :

‖a‖ ≠ 0 → a ≠ 0

theorem norm_of_subsingleton' {E : Type u_4} [SeminormedGroup E] [Subsingleton E] (a : E) :

‖a‖ = 0

theorem norm_of_subsingleton {E : Type u_4} [SeminormedAddGroup E] [Subsingleton E] (a : E) :

‖a‖ = 0

theorem zero_lt_one_add_norm_sq' {E : Type u_4} [SeminormedGroup E] (x : E) :

0 < 1 + ‖x‖ ^ 2

theorem zero_lt_one_add_norm_sq {E : Type u_4} [SeminormedAddGroup E] (x : E) :

0 < 1 + ‖x‖ ^ 2

theorem norm_div_le {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a / b‖ ≤ ‖a‖ + ‖b‖

theorem norm_sub_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a - b‖ ≤ ‖a‖ + ‖b‖

theorem norm_div_le_of_le {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] (a b : E) :

dist a b ≤ ‖a‖ + ‖b‖

theorem dist_le_norm_add_norm {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

dist a b ≤ ‖a‖ + ‖b‖

theorem abs_norm_sub_norm_le_norm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

|‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖

theorem abs_norm_sub_norm_le_norm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

|‖a‖ - ‖b‖| ≤ ‖-a + b‖

theorem norm_sub_norm_le_norm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖a⁻¹ * b‖

theorem norm_sub_norm_le_norm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖-a + b‖

theorem norm_sub_le_norm_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖a * b‖

theorem norm_sub_le_norm_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖a + b‖

theorem dist_norm_norm_le_norm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

dist ‖a‖ ‖b‖ ≤ ‖a⁻¹ * b‖

theorem dist_norm_norm_le_norm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

dist ‖a‖ ‖b‖ ≤ ‖-a + b‖

theorem norm_le_norm_add_norm_div' {E : Type u_4} [SeminormedGroup E] (u v : E) :

‖u‖ ≤ ‖v‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub' {E : Type u_4} [SeminormedAddGroup E] (u v : E) :

‖u‖ ≤ ‖v‖ + ‖u - v‖

theorem norm_le_norm_add_norm_inv_mul {E : Type u_4} [SeminormedGroup E] (u v : E) :

‖u‖ ≤ ‖v‖ + ‖u⁻¹ * v‖

theorem norm_le_norm_add_norm_neg_add {E : Type u_4} [SeminormedAddGroup E] (u v : E) :

‖u‖ ≤ ‖v‖ + ‖-u + v‖

theorem norm_le_norm_add_norm_div {E : Type u_4} [SeminormedGroup E] (u v : E) :

‖v‖ ≤ ‖u‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub {E : Type u_4} [SeminormedAddGroup E] (u v : E) :

‖v‖ ≤ ‖u‖ + ‖u - v‖

theorem norm_le_insert' {E : Type u_4} [SeminormedAddGroup E] (u v : E) :

‖u‖ ≤ ‖v‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub'.

theorem norm_le_insert {E : Type u_4} [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_4} [SeminormedGroup E] (u v : E) :

‖u‖ ≤ ‖u * v‖ + ‖v‖

theorem norm_le_add_norm_add {E : Type u_4} [SeminormedAddGroup E] (u v : E) :

‖u‖ ≤ ‖u + v‖ + ‖v‖

theorem norm_le_mul_norm_add' {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖ = 0) :

‖x * y‖ = ‖y‖

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

‖x + y‖ = ‖y‖

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

‖x * y‖ = ‖x‖

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

‖x + y‖ = ‖x‖

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

‖x / y‖ = ‖y‖

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

‖x - y‖ = ‖y‖

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

‖x / y‖ = ‖x‖

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

‖x - y‖ = ‖x‖

theorem ball_eq_norm_inv_mul_lt {E : Type u_4} [SeminormedGroup E] (y : E) (ε : ℝ) :

Metric.ball y ε = {x : E | ‖x⁻¹ * y‖ < ε}

theorem ball_eq_norm_neg_add_lt {E : Type u_4} [SeminormedAddGroup E] (y : E) (ε : ℝ) :

Metric.ball y ε = {x : E | ‖-x + y‖ < ε}

theorem ball_one_eq {E : Type u_4} [SeminormedGroup E] (r : ℝ) :

Metric.ball 1 r = {x : E | ‖x‖ < r}

theorem ball_zero_eq {E : Type u_4} [SeminormedAddGroup E] (r : ℝ) :

Metric.ball 0 r = {x : E | ‖x‖ < r}

theorem mem_ball_iff_norm_inv_mul_lt {E : Type u_4} [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_4} [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_4} [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_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.ball a r ↔ ‖-a + b‖ < r

theorem mem_ball_one_iff {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} :

a ∈ Metric.ball 1 r ↔ ‖a‖ < r

theorem mem_ball_zero_iff {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} :

a ∈ Metric.ball 0 r ↔ ‖a‖ < r

theorem mem_closedBall_iff_norm_inv_mul_le {E : Type u_4} [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_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖-b + a‖ ≤ r

theorem mem_closedBall_one_iff {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} :

a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_zero_iff {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} :

a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_iff_norm_inv_mul_le' {E : Type u_4} [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_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖-a + b‖ ≤ r

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

‖b‖ ≤ ‖a‖ + r

theorem norm_le_of_mem_closedBall {E : Type u_4} [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_4} [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_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} :

dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

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

‖b‖ < ‖a‖ + r

theorem norm_lt_of_mem_ball {E : Type u_4} [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_4} [SeminormedGroup E] (u v w : E) :

‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_4} [SeminormedAddGroup E] (u v w : E) :

‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖

theorem norm_mul_sub_norm_div_le_two_mul {E : Type u_7} [SeminormedGroup E] (u v : E) :

‖u * v‖ - ‖u / v‖ ≤ 2 * ‖v‖

theorem norm_add_sub_norm_sub_le_two_mul {E : Type u_7} [SeminormedAddGroup E] (u v : E) :

‖u + v‖ - ‖u - v‖ ≤ 2 * ‖v‖

theorem norm_mul_sub_norm_div_le_two_mul_min {E : Type u_7} [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_7} [SeminormedAddCommGroup E] (u v : E) :

‖u + v‖ - ‖u - v‖ ≤ 2 * min ‖u‖ ‖v‖

theorem mem_sphere_iff_norm_inv_mul_eq {E : Type u_4} [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_4} [SeminormedAddGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.sphere a r ↔ ‖-b + a‖ = r

theorem mem_sphere_one_iff_norm {E : Type u_4} [SeminormedGroup E] {a : E} {r : ℝ} :

a ∈ Metric.sphere 1 r ↔ ‖a‖ = r

theorem mem_sphere_zero_iff_norm {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ℝ} :

a ∈ Metric.sphere 0 r ↔ ‖a‖ = r

@[simp]

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

‖↑x‖ = r

@[simp]

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

‖↑x‖ = r

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

↑x ≠ 1

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

↑x ≠ 0

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

↑x ≠ 1

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

↑x ≠ 0

def normGroupSeminorm (E : Type u_4) [SeminormedGroup E] :

GroupSeminorm E

The norm of a seminormed group as a group seminorm.

Equations

normGroupSeminorm E = { toFun := norm, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }

Instances For

def normAddGroupSeminorm (E : Type u_4) [SeminormedAddGroup E] :

AddGroupSeminorm E

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

Equations

normAddGroupSeminorm E = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }

Instances For

@[simp]

theorem coe_normGroupSeminorm (E : Type u_4) [SeminormedGroup E] :

⇑(normGroupSeminorm E) = norm

@[simp]

theorem coe_normAddGroupSeminorm (E : Type u_4) [SeminormedAddGroup E] :

⇑(normAddGroupSeminorm E) = norm

theorem NormedGroup.tendsto_nhds_one {α : Type u_2} {E : Type u_4} [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_4} [SeminormedAddGroup E] {f : α → E} {l : Filter α} :

Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

theorem NormedGroup.tendsto_nhds_nhds {E : Type u_4} {F : Type u_5} [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_4} {F : Type u_5} [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_4} [SeminormedGroup E] (x : E) :

(nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y⁻¹ * x‖ < ε}

theorem NormedAddGroup.nhds_basis_norm_lt {E : Type u_4} [SeminormedAddGroup E] (x : E) :

(nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖-y + x‖ < ε}

theorem NormedGroup.nhds_one_basis_norm_lt {E : Type u_4} [SeminormedGroup E] :

(nhds 1).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

theorem NormedAddGroup.nhds_zero_basis_norm_lt {E : Type u_4} [SeminormedAddGroup E] :

(nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

theorem NormedGroup.uniformity_basis_dist {E : Type u_4} [SeminormedGroup E] :

(uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1⁻¹ * p.2‖ < ε}

theorem NormedAddGroup.uniformity_basis_dist {E : Type u_4} [SeminormedAddGroup E] :

(uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖-p.1 + p.2‖ < ε}

@[instance_reducible, instance 100]

instance SeminormedGroup.toNNNorm {E : Type u_4} [SeminormedGroup E] :

NNNorm E

Equations

SeminormedGroup.toNNNorm = { nnNorm := fun (a : E) => NNReal.mk ‖a‖ ⋯ }

@[instance_reducible, instance 100]

instance SeminormedAddGroup.toNNNorm {E : Type u_4} [SeminormedAddGroup E] :

NNNorm E

Equations

SeminormedAddGroup.toNNNorm = { nnNorm := fun (a : E) => NNReal.mk ‖a‖ ⋯ }

@[simp]

theorem coe_nnNorm' {E : Type u_4} [SeminormedGroup E] (a : E) :

↑‖a‖₊ = ‖a‖

@[simp]

theorem coe_nnNorm {E : Type u_4} [SeminormedAddGroup E] (a : E) :

↑‖a‖₊ = ‖a‖

@[deprecated coe_nnNorm' (since := "2026-10-31")]

theorem coe_nnnorm' {E : Type u_4} [SeminormedGroup E] (a : E) :

↑‖a‖₊ = ‖a‖

Alias of coe_nnNorm'.

@[deprecated coe_nnNorm (since := "2026-10-31")]

theorem coe_nnnorm {E : Type u_4} [SeminormedAddGroup E] (a : E) :

↑‖a‖₊ = ‖a‖

Alias of coe_nnNorm.

@[simp]

theorem coe_comp_nnNorm' {E : Type u_4} [SeminormedGroup E] :

@[simp]

theorem coe_comp_nnNorm {E : Type u_4} [SeminormedAddGroup E] :

@[deprecated coe_comp_nnNorm' (since := "2026-10-31")]

theorem coe_comp_nnnorm' {E : Type u_4} [SeminormedGroup E] :

Alias of coe_comp_nnNorm'.

@[deprecated coe_comp_nnNorm (since := "2026-10-31")]

theorem coe_comp_nnnorm {E : Type u_4} [SeminormedAddGroup E] :

Alias of coe_comp_nnNorm.

@[simp]

theorem norm_toNNReal' {E : Type u_4} [SeminormedGroup E] {a : E} :

‖a‖.toNNReal = ‖a‖₊

@[simp]

theorem norm_toNNReal {E : Type u_4} [SeminormedAddGroup E] {a : E} :

‖a‖.toNNReal = ‖a‖₊

@[simp]

theorem toReal_enorm' {E : Type u_4} [SeminormedGroup E] (x : E) :

‖x‖ₑ.toReal = ‖x‖

@[simp]

theorem toReal_enorm {E : Type u_4} [SeminormedAddGroup E] (x : E) :

‖x‖ₑ.toReal = ‖x‖

@[simp]

theorem ofReal_norm' {E : Type u_4} [SeminormedGroup E] (x : E) :

@[simp]

theorem ofReal_norm {E : Type u_4} [SeminormedAddGroup E] (x : E) :

@[deprecated ofReal_norm (since := "2026-05-25")]

theorem ofReal_norm_eq_enorm {E : Type u_4} [SeminormedAddGroup E] (x : E) :

Alias of ofReal_norm.

@[deprecated ofReal_norm' (since := "2026-05-25")]

theorem ofReal_norm_eq_enorm' {E : Type u_4} [SeminormedGroup E] (x : E) :

Alias of ofReal_norm'.

theorem enorm'_eq_iff_norm_eq {E : Type u_4} {F : Type u_5} [SeminormedGroup E] [SeminormedGroup F] {x : E} {y : F} :

‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

theorem enorm_eq_iff_norm_eq {E : Type u_4} {F : Type u_5} [SeminormedAddGroup E] [SeminormedAddGroup F] {x : E} {y : F} :

‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

theorem enorm'_le_iff_norm_le {E : Type u_4} {F : Type u_5} [SeminormedGroup E] [SeminormedGroup F] {x : E} {y : F} :

‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

theorem enorm_le_iff_norm_le {E : Type u_4} {F : Type u_5} [SeminormedAddGroup E] [SeminormedAddGroup F] {x : E} {y : F} :

‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

theorem nnDist_eq_nnNorm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

nndist a b = ‖a⁻¹ * b‖₊

theorem nnDist_eq_nnNorm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

nndist a b = ‖-a + b‖₊

@[deprecated nnDist_eq_nnNorm_inv_mul (since := "2026-10-31")]

theorem nndist_eq_nnnorm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

nndist a b = ‖a⁻¹ * b‖₊

Alias of nnDist_eq_nnNorm_inv_mul.

@[deprecated nnDist_eq_nnNorm_neg_add (since := "2026-10-31")]

theorem nndist_eq_nnnorm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

nndist a b = ‖-a + b‖₊

Alias of nnDist_eq_nnNorm_neg_add.

@[simp]

theorem nnNorm_inv' {E : Type u_4} [SeminormedGroup E] (a : E) :

‖a⁻¹ ‖₊ = ‖a‖₊

@[simp]

theorem nnNorm_neg {E : Type u_4} [SeminormedAddGroup E] (a : E) :

‖-a‖₊ = ‖a‖₊

@[deprecated nnNorm_inv' (since := "2026-10-31")]

theorem nnnorm_inv' {E : Type u_4} [SeminormedGroup E] (a : E) :

‖a⁻¹ ‖₊ = ‖a‖₊

Alias of nnNorm_inv'.

@[deprecated nnNorm_neg (since := "2026-10-31")]

theorem nnnorm_neg {E : Type u_4} [SeminormedAddGroup E] (a : E) :

‖-a‖₊ = ‖a‖₊

Alias of nnNorm_neg.

@[simp]

theorem nndist_one_right {E : Type u_4} [SeminormedGroup E] (a : E) :

nndist a 1 = ‖a‖₊

@[simp]

theorem nndist_zero_right {E : Type u_4} [SeminormedAddGroup E] (a : E) :

nndist a 0 = ‖a‖₊

@[simp]

theorem edist_one_right {E : Type u_4} [SeminormedGroup E] (a : E) :

edist a 1 = ‖a‖ₑ

@[simp]

theorem edist_zero_right {E : Type u_4} [SeminormedAddGroup E] (a : E) :

edist a 0 = ‖a‖ₑ

@[simp]

theorem nnNorm_one' {E : Type u_4} [SeminormedGroup E] :

‖1‖₊ = 0

@[simp]

theorem nnNorm_zero {E : Type u_4} [SeminormedAddGroup E] :

‖0‖₊ = 0

@[deprecated nnNorm_one' (since := "2026-10-31")]

theorem nnnorm_one' {E : Type u_4} [SeminormedGroup E] :

‖1‖₊ = 0

Alias of nnNorm_one'.

@[deprecated nnNorm_zero (since := "2026-10-31")]

theorem nnnorm_zero {E : Type u_4} [SeminormedAddGroup E] :

‖0‖₊ = 0

Alias of nnNorm_zero.

theorem ne_one_of_nnNorm_ne_zero {E : Type u_4} [SeminormedGroup E] {a : E} :

‖a‖₊ ≠ 0 → a ≠ 1

theorem ne_zero_of_nnNorm_ne_zero {E : Type u_4} [SeminormedAddGroup E] {a : E} :

‖a‖₊ ≠ 0 → a ≠ 0

@[deprecated ne_one_of_nnNorm_ne_zero (since := "2026-10-31")]

theorem ne_one_of_nnnorm_ne_zero {E : Type u_4} [SeminormedGroup E] {a : E} :

‖a‖₊ ≠ 0 → a ≠ 1

Alias of ne_one_of_nnNorm_ne_zero.

@[deprecated ne_zero_of_nnNorm_ne_zero (since := "2026-10-31")]

theorem ne_zero_of_nnnorm_ne_zero {E : Type u_4} [SeminormedAddGroup E] {a : E} :

‖a‖₊ ≠ 0 → a ≠ 0

Alias of ne_zero_of_nnNorm_ne_zero.

theorem nnNorm_mul_le' {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnNorm_add_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊

@[deprecated nnNorm_mul_le' (since := "2026-10-31")]

theorem nnnorm_mul_le' {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Alias of nnNorm_mul_le'.

@[deprecated nnNorm_add_le (since := "2026-10-31")]

theorem nnnorm_add_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Alias of nnNorm_add_le.

theorem norm_pow_le_mul_norm {E : Type u_4} [SeminormedGroup E] {a : E} {n : ℕ} :

‖a ^ n‖ ≤ ↑n * ‖a‖

theorem norm_nsmul_le {E : Type u_4} [SeminormedAddGroup E] {a : E} {n : ℕ} :

‖n • a‖ ≤ ↑n * ‖a‖

theorem nnNorm_pow_le_mul_norm {E : Type u_4} [SeminormedGroup E] {a : E} {n : ℕ} :

‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

theorem nnNorm_nsmul_le {E : Type u_4} [SeminormedAddGroup E] {a : E} {n : ℕ} :

‖n • a‖₊ ≤ ↑n * ‖a‖₊

@[deprecated nnNorm_pow_le_mul_norm (since := "2026-10-31")]

theorem nnnorm_pow_le_mul_norm {E : Type u_4} [SeminormedGroup E] {a : E} {n : ℕ} :

‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

Alias of nnNorm_pow_le_mul_norm.

@[deprecated nnNorm_nsmul_le (since := "2026-10-31")]

theorem nnnorm_nsmul_le {E : Type u_4} [SeminormedAddGroup E] {a : E} {n : ℕ} :

‖n • a‖₊ ≤ ↑n * ‖a‖₊

Alias of nnNorm_nsmul_le.

@[simp]

theorem nnNorm_zpow_abs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ |n|‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnNorm_abs_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖|n| • a‖₊ = ‖n • a‖₊

@[deprecated nnNorm_zpow_abs (since := "2026-10-31")]

theorem nnnorm_zpow_abs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ |n|‖₊ = ‖a ^ n‖₊

Alias of nnNorm_zpow_abs.

@[deprecated nnNorm_abs_zsmul (since := "2026-10-31")]

theorem nnnorm_abs_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖|n| • a‖₊ = ‖n • a‖₊

Alias of nnNorm_abs_zsmul.

@[simp]

theorem nnNorm_pow_natAbs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnNorm_natAbs_smul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖n.natAbs • a‖₊ = ‖n • a‖₊

@[deprecated nnNorm_pow_natAbs (since := "2026-10-31")]

theorem nnnorm_pow_natAbs {E : Type u_4} [SeminormedGroup E] (a : E) (n : ℤ) :

‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

Alias of nnNorm_pow_natAbs.

@[deprecated nnNorm_natAbs_smul (since := "2026-10-31")]

theorem nnnorm_natAbs_smul {E : Type u_4} [SeminormedAddGroup E] (a : E) (n : ℤ) :

‖n.natAbs • a‖₊ = ‖n • a‖₊

Alias of nnNorm_natAbs_smul.

theorem nnNorm_zpow_isUnit {E : Type u_4} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

‖a ^ n‖₊ = ‖a‖₊

theorem nnNorm_isUnit_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

@[deprecated nnNorm_zpow_isUnit (since := "2026-10-31")]

theorem nnnorm_zpow_isUnit {E : Type u_4} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

‖a ^ n‖₊ = ‖a‖₊

Alias of nnNorm_zpow_isUnit.

@[deprecated nnNorm_isUnit_zsmul (since := "2026-10-31")]

theorem nnnorm_isUnit_zsmul {E : Type u_4} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) :

Alias of nnNorm_isUnit_zsmul.

@[simp]

theorem nnNorm_units_zsmul {E : Type u_7} [SeminormedAddGroup E] (n : ℤ ˣ) (a : E) :

@[deprecated nnNorm_units_zsmul (since := "2026-10-31")]

theorem nnnorm_units_zsmul {E : Type u_7} [SeminormedAddGroup E] (n : ℤ ˣ) (a : E) :

Alias of nnNorm_units_zsmul.

@[simp]

theorem nndist_one_left {E : Type u_4} [SeminormedGroup E] (a : E) :

nndist 1 a = ‖a‖₊

@[simp]

theorem nndist_zero_left {E : Type u_4} [SeminormedAddGroup E] (a : E) :

nndist 0 a = ‖a‖₊

@[simp]

theorem edist_one_left {E : Type u_4} [SeminormedGroup E] (a : E) :

edist 1 a = ↑‖a‖₊

@[simp]

theorem edist_zero_left {E : Type u_4} [SeminormedAddGroup E] (a : E) :

edist 0 a = ↑‖a‖₊

theorem nndist_mulIndicator {α : Type u_2} {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] (a b : E) :

‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnNorm_sub_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊

@[deprecated nnNorm_div_le (since := "2026-10-31")]

theorem nnnorm_div_le {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Alias of nnNorm_div_le.

@[deprecated nnNorm_sub_le (since := "2026-10-31")]

theorem nnnorm_sub_le {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊

Alias of nnNorm_sub_le.

theorem enorm_div_le {E : Type u_4} [SeminormedGroup E] {a b : E} :

‖a / b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_sub_le {E : Type u_4} [SeminormedAddGroup E] {a b : E} :

‖a - b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem nnDist_nnNorm_nnNorm_le_nnNorm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a⁻¹ * b‖₊

theorem nnDist_nnNorm_nnNorm_le_nnNorm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖-a + b‖₊

@[deprecated nnDist_nnNorm_nnNorm_le_nnNorm_inv_mul (since := "2026-10-31")]

theorem nndist_nnnorm_nnnorm_le_nnnorm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a⁻¹ * b‖₊

Alias of nnDist_nnNorm_nnNorm_le_nnNorm_inv_mul.

@[deprecated nnDist_nnNorm_nnNorm_le_nnNorm_neg_add (since := "2026-10-31")]

theorem nndist_nnnorm_nnnorm_le_nnnorm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖-a + b‖₊

Alias of nnDist_nnNorm_nnNorm_le_nnNorm_neg_add.

theorem nnNorm_le_nnNorm_add_nnNorm_div {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

theorem nnNorm_le_nnNorm_add_nnNorm_sub {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

@[deprecated nnNorm_le_nnNorm_add_nnNorm_div (since := "2026-10-31")]

theorem nnnorm_le_nnnorm_add_nnnorm_div {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

Alias of nnNorm_le_nnNorm_add_nnNorm_div.

@[deprecated nnNorm_le_nnNorm_add_nnNorm_sub (since := "2026-10-31")]

theorem nnnorm_le_nnnorm_add_nnnorm_sub {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_nnNorm_add_nnNorm_sub.

theorem nnNorm_le_nnNorm_add_nnNorm_div' {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

theorem nnNorm_le_nnNorm_add_nnNorm_sub' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

@[deprecated nnNorm_le_nnNorm_add_nnNorm_div' (since := "2026-10-31")]

theorem nnnorm_le_nnnorm_add_nnnorm_div' {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

Alias of nnNorm_le_nnNorm_add_nnNorm_div'.

@[deprecated nnNorm_le_nnNorm_add_nnNorm_sub' (since := "2026-10-31")]

theorem nnnorm_le_nnnorm_add_nnnorm_sub' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_nnNorm_add_nnNorm_sub'.

theorem nnNorm_le_insert' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_nnNorm_add_nnNorm_sub'.

@[deprecated nnNorm_le_insert' (since := "2026-10-31")]

theorem nnnorm_le_insert' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_insert'.

Alias of nnNorm_le_nnNorm_add_nnNorm_sub'.

theorem nnNorm_le_insert {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_nnNorm_add_nnNorm_sub.

@[deprecated nnNorm_le_insert (since := "2026-10-31")]

theorem nnnorm_le_insert {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

Alias of nnNorm_le_insert.

Alias of nnNorm_le_nnNorm_add_nnNorm_sub.

theorem nnNorm_le_mul_nnNorm_add {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

theorem nnNorm_le_add_nnNorm_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊

@[deprecated nnNorm_le_mul_nnNorm_add (since := "2026-10-31")]

theorem nnnorm_le_mul_nnnorm_add {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

Alias of nnNorm_le_mul_nnNorm_add.

@[deprecated nnNorm_le_add_nnNorm_add (since := "2026-10-31")]

theorem nnnorm_le_add_nnnorm_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊

Alias of nnNorm_le_add_nnNorm_add.

theorem nnNorm_le_mul_nnNorm_add' {E : Type u_4} [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_4} [SeminormedAddGroup E] (a b : E) :

‖b‖₊ ≤ ‖a + b‖₊ + ‖a‖₊

An analogue of nnNorm_le_add_nnNorm_add for the addition from the left.

@[deprecated nnNorm_le_mul_nnNorm_add' (since := "2026-10-31")]

theorem nnnorm_le_mul_nnnorm_add' {E : Type u_4} [SeminormedGroup E] (a b : E) :

‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊

Alias of nnNorm_le_mul_nnNorm_add'.

An analogue of nnNorm_le_mul_nnNorm_add for the multiplication from the left.

@[deprecated nnNorm_le_add_nnNorm_add' (since := "2026-10-31")]

theorem nnnorm_le_add_nnnorm_add' {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

‖b‖₊ ≤ ‖a + b‖₊ + ‖a‖₊

Alias of nnNorm_le_add_nnNorm_add'.

An analogue of nnNorm_le_add_nnNorm_add for the addition from the left.

theorem nnNorm_mul_eq_nnNorm_right {E : Type u_4} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) :

‖x * y‖₊ = ‖y‖₊

theorem nnNorm_add_eq_nnNorm_right {E : Type u_4} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) :

‖x + y‖₊ = ‖y‖₊

@[deprecated nnNorm_mul_eq_nnNorm_right (since := "2026-10-31")]

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

‖x * y‖₊ = ‖y‖₊

Alias of nnNorm_mul_eq_nnNorm_right.

@[deprecated nnNorm_add_eq_nnNorm_right (since := "2026-10-31")]

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

‖x + y‖₊ = ‖y‖₊

Alias of nnNorm_add_eq_nnNorm_right.

theorem nnNorm_mul_eq_nnNorm_left {E : Type u_4} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) :

‖x * y‖₊ = ‖x‖₊

theorem nnNorm_add_eq_nnNorm_left {E : Type u_4} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) :

‖x + y‖₊ = ‖x‖₊

@[deprecated nnNorm_mul_eq_nnNorm_left (since := "2026-10-31")]

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

‖x * y‖₊ = ‖x‖₊

Alias of nnNorm_mul_eq_nnNorm_left.

@[deprecated nnNorm_add_eq_nnNorm_left (since := "2026-10-31")]

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

‖x + y‖₊ = ‖x‖₊

Alias of nnNorm_add_eq_nnNorm_left.

theorem nnNorm_div_eq_nnNorm_right {E : Type u_4} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) :

‖x / y‖₊ = ‖y‖₊

theorem nnNorm_sub_eq_nnNorm_right {E : Type u_4} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) :

‖x - y‖₊ = ‖y‖₊

@[deprecated nnNorm_div_eq_nnNorm_right (since := "2026-10-31")]

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

‖x / y‖₊ = ‖y‖₊

Alias of nnNorm_div_eq_nnNorm_right.

@[deprecated nnNorm_sub_eq_nnNorm_right (since := "2026-10-31")]

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

‖x - y‖₊ = ‖y‖₊

Alias of nnNorm_sub_eq_nnNorm_right.

theorem nnNorm_div_eq_nnNorm_left {E : Type u_4} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) :

‖x / y‖₊ = ‖x‖₊

theorem nnNorm_sub_eq_nnNorm_left {E : Type u_4} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) :

‖x - y‖₊ = ‖x‖₊

@[deprecated nnNorm_div_eq_nnNorm_left (since := "2026-10-31")]

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

‖x / y‖₊ = ‖x‖₊

Alias of nnNorm_div_eq_nnNorm_left.

@[deprecated nnNorm_sub_eq_nnNorm_left (since := "2026-10-31")]

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

‖x - y‖₊ = ‖x‖₊

Alias of nnNorm_sub_eq_nnNorm_left.

theorem toReal_coe_nnNorm' {E : Type u_4} [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_4} [SeminormedAddGroup E] (a : E) :

(↑‖a‖₊).toReal = ‖a‖

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

@[deprecated toReal_coe_nnNorm' (since := "2026-10-31")]

theorem toReal_coe_nnnorm' {E : Type u_4} [SeminormedGroup E] (a : E) :

(↑‖a‖₊).toReal = ‖a‖

Alias of toReal_coe_nnNorm'.

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

@[deprecated toReal_coe_nnNorm (since := "2026-10-31")]

theorem toReal_coe_nnnorm {E : Type u_4} [SeminormedAddGroup E] (a : E) :

(↑‖a‖₊).toReal = ‖a‖

Alias of toReal_coe_nnNorm.

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_4} [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_4} [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_4} [SeminormedGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

theorem nontrivialTopology_iff_exists_nnNorm_ne_zero {E : Type u_4} [SeminormedAddGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

@[deprecated nontrivialTopology_iff_exists_nnNorm_ne_zero' (since := "2026-10-31")]

theorem nontrivialTopology_iff_exists_nnnorm_ne_zero' {E : Type u_4} [SeminormedGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

Alias of nontrivialTopology_iff_exists_nnNorm_ne_zero'.

@[deprecated nontrivialTopology_iff_exists_nnNorm_ne_zero (since := "2026-10-31")]

theorem nontrivialTopology_iff_exists_nnnorm_ne_zero {E : Type u_4} [SeminormedAddGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖₊ ≠ 0

Alias of nontrivialTopology_iff_exists_nnNorm_ne_zero.

theorem indiscreteTopology_iff_forall_nnNorm_eq_zero' {E : Type u_4} [SeminormedGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

theorem indiscreteTopology_iff_forall_nnNorm_eq_zero {E : Type u_4} [SeminormedAddGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

@[deprecated indiscreteTopology_iff_forall_nnNorm_eq_zero' (since := "2026-10-31")]

theorem indiscreteTopology_iff_forall_nnnorm_eq_zero' {E : Type u_4} [SeminormedGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

Alias of indiscreteTopology_iff_forall_nnNorm_eq_zero'.

@[deprecated indiscreteTopology_iff_forall_nnNorm_eq_zero (since := "2026-10-31")]

theorem indiscreteTopology_iff_forall_nnnorm_eq_zero {E : Type u_4} [SeminormedAddGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖₊ = 0

Alias of indiscreteTopology_iff_forall_nnNorm_eq_zero.

theorem exists_nnNorm_ne_zero' (E : Type u_4) [SeminormedGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖₊ ≠ 0

theorem exists_nnNorm_ne_zero (E : Type u_4) [SeminormedAddGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖₊ ≠ 0

@[deprecated exists_nnNorm_ne_zero' (since := "2026-10-31")]

theorem exists_nnnorm_ne_zero' (E : Type u_4) [SeminormedGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖₊ ≠ 0

Alias of exists_nnNorm_ne_zero'.

@[deprecated exists_nnNorm_ne_zero (since := "2026-10-31")]

theorem exists_nnnorm_ne_zero (E : Type u_4) [SeminormedAddGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖₊ ≠ 0

Alias of exists_nnNorm_ne_zero.

theorem IndiscreteTopology.nnNorm_eq_zero' {E : Type u_4} [SeminormedGroup E] [IndiscreteTopology E] (x : E) :

theorem IndiscreteTopology.nnNorm_eq_zero {E : Type u_4} [SeminormedAddGroup E] [IndiscreteTopology E] (x : E) :

@[deprecated IndiscreteTopology.nnNorm_eq_zero' (since := "2026-10-31")]

theorem IndiscreteTopology.nnnorm_eq_zero' {E : Type u_4} [SeminormedGroup E] [IndiscreteTopology E] (x : E) :

Alias of IndiscreteTopology.nnNorm_eq_zero'.

@[deprecated IndiscreteTopology.nnNorm_eq_zero (since := "2026-10-31")]

theorem IndiscreteTopology.nnnorm_eq_zero {E : Type u_4} [SeminormedAddGroup E] [IndiscreteTopology E] (x : E) :

Alias of IndiscreteTopology.nnNorm_eq_zero.

theorem NontrivialTopology.of_exists_nnNorm_ne_zero' {E : Type u_4} [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_4} [SeminormedAddGroup E] :

(∃ (x : E), ‖x‖₊ ≠ 0) → NontrivialTopology E

Alias of the reverse direction of nontrivialTopology_iff_exists_nnNorm_ne_zero.

@[deprecated NontrivialTopology.of_exists_nnNorm_ne_zero' (since := "2026-11-01")]

theorem NontrivialTopology.of_exists_nnnorm_ne_zero' {E : Type u_4} [SeminormedGroup E] :

(∃ (x : E), ‖x‖₊ ≠ 0) → NontrivialTopology E

Alias of NontrivialTopology.of_exists_nnNorm_ne_zero'.

Alias of the reverse direction of nontrivialTopology_iff_exists_nnNorm_ne_zero'.

@[deprecated NontrivialTopology.of_exists_nnNorm_ne_zero (since := "2026-11-01")]

theorem NontrivialTopology.of_exists_nnnorm_ne_zero {E : Type u_4} [SeminormedAddGroup E] :

(∃ (x : E), ‖x‖₊ ≠ 0) → NontrivialTopology E

Alias of NontrivialTopology.of_exists_nnNorm_ne_zero.

Alias of the reverse direction of nontrivialTopology_iff_exists_nnNorm_ne_zero.

theorem IndiscreteTopology.of_forall_nnNorm_eq_zero' {E : Type u_4} [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_4} [SeminormedAddGroup E] :

(∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E

Alias of the reverse direction of indiscreteTopology_iff_forall_nnNorm_eq_zero.

@[deprecated IndiscreteTopology.of_forall_nnNorm_eq_zero' (since := "2026-11-01")]

theorem IndiscreteTopology.of_forall_nnnorm_eq_zero' {E : Type u_4} [SeminormedGroup E] :

(∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E

Alias of IndiscreteTopology.of_forall_nnNorm_eq_zero'.

Alias of the reverse direction of indiscreteTopology_iff_forall_nnNorm_eq_zero'.

@[deprecated IndiscreteTopology.of_forall_nnNorm_eq_zero (since := "2026-11-01")]

theorem IndiscreteTopology.of_forall_nnnorm_eq_zero {E : Type u_4} [SeminormedAddGroup E] :

(∀ (x : E), ‖x‖₊ = 0) → IndiscreteTopology E

Alias of IndiscreteTopology.of_forall_nnNorm_eq_zero.

Alias of the reverse direction of indiscreteTopology_iff_forall_nnNorm_eq_zero.

theorem nontrivialTopology_iff_exists_norm_ne_zero' {E : Type u_4} [SeminormedGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖ ≠ 0

theorem nontrivialTopology_iff_exists_norm_ne_zero {E : Type u_4} [SeminormedAddGroup E] :

NontrivialTopology E ↔ ∃ (x : E), ‖x‖ ≠ 0

theorem indiscreteTopology_iff_forall_norm_eq_zero' {E : Type u_4} [SeminormedGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

theorem indiscreteTopology_iff_forall_norm_eq_zero {E : Type u_4} [SeminormedAddGroup E] :

IndiscreteTopology E ↔ ∀ (x : E), ‖x‖ = 0

theorem exists_norm_ne_zero' (E : Type u_4) [SeminormedGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖ ≠ 0

theorem exists_norm_ne_zero (E : Type u_4) [SeminormedAddGroup E] [NontrivialTopology E] :

∃ (x : E), ‖x‖ ≠ 0

theorem IndiscreteTopology.norm_eq_zero' {E : Type u_4} [SeminormedGroup E] [IndiscreteTopology E] (x : E) :

‖x‖ = 0

theorem IndiscreteTopology.norm_eq_zero {E : Type u_4} [SeminormedAddGroup E] [IndiscreteTopology E] (x : E) :

‖x‖ = 0

theorem NontrivialTopology.of_exists_norm_ne_zero' {E : Type u_4} [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_4} [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_4} [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_4} [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_7} [TopologicalSpace E] [ESeminormedMonoid E] :

‖1‖ₑ = 0

@[simp]

theorem enorm_zero {E : Type u_7} [TopologicalSpace E] [ESeminormedAddMonoid E] :

‖0‖ₑ = 0

theorem exists_enorm_lt' (E : Type u_7) [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_7) [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_4} [SeminormedGroup E] (a : E) :

‖a⁻¹ ‖ₑ = ‖a‖ₑ

@[simp]

theorem enorm_neg {E : Type u_4} [SeminormedAddGroup E] (a : E) :

‖-a‖ₑ = ‖a‖ₑ

theorem edist_eq_enorm_inv_mul {E : Type u_4} [SeminormedGroup E] (a b : E) :

edist a b = ‖a⁻¹ * b‖ₑ

theorem edist_eq_enorm_neg_add {E : Type u_4} [SeminormedAddGroup E] (a b : E) :

edist a b = ‖-a + b‖ₑ

theorem enorm_div_rev {E : Type u_7} [SeminormedGroup E] (a b : E) :

‖a / b‖ₑ = ‖b / a‖ₑ

theorem enorm_sub_rev {E : Type u_7} [SeminormedAddGroup E] (a b : E) :

‖a - b‖ₑ = ‖b - a‖ₑ

theorem mem_eball_one_iff {E : Type u_4} [SeminormedGroup E] {a : E} {r : ENNReal} :

a ∈ Metric.eball 1 r ↔ ‖a‖ₑ < r

theorem mem_eball_zero_iff {E : Type u_4} [SeminormedAddGroup E] {a : E} {r : ENNReal} :

a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r

theorem enorm_mul_le' {E : Type u_7} [TopologicalSpace E] [ESeminormedMonoid E] (a b : E) :

‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_add_le {E : Type u_7} [TopologicalSpace E] [ESeminormedAddMonoid E] (a b : E) :

‖a + b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ

theorem enorm_mul_le_of_le' {E : Type u_7} [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_7} [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_7} [TopologicalSpace E] [ESeminormedMonoid E] {a b c : E} :

‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ

theorem enorm_add₃_le {E : Type u_7} [TopologicalSpace E] [ESeminormedAddMonoid E] {a b c : E} :

‖a + b + c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ

theorem enorm_mul₄_le' {E : Type u_7} [TopologicalSpace E] [ESeminormedMonoid E] {a b c d : E} :

‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ

theorem enorm_add₄_le {E : Type u_7} [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_7} [TopologicalSpace E] [ENormedMonoid E] {a : E} :

‖a‖ₑ = 0 ↔ a = 1

@[simp]

theorem enorm_eq_zero {E : Type u_7} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} :

‖a‖ₑ = 0 ↔ a = 0

theorem enorm_ne_zero' {E : Type u_7} [TopologicalSpace E] [ENormedMonoid E] {a : E} :

‖a‖ₑ ≠ 0 ↔ a ≠ 1

theorem enorm_ne_zero {E : Type u_7} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} :

‖a‖ₑ ≠ 0 ↔ a ≠ 0

@[simp]

theorem enorm_pos' {E : Type u_7} [TopologicalSpace E] [ENormedMonoid E] {a : E} :

0 < ‖a‖ₑ ↔ a ≠ 1

@[simp]

theorem enorm_pos {E : Type u_7} [TopologicalSpace E] [ENormedAddMonoid E] {a : E} :

0 < ‖a‖ₑ ↔ a ≠ 0

theorem SeminormedGroup.disjoint_nhds {E : Type u_4} [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_4} [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_4} [SeminormedGroup E] (f : Filter E) :

Disjoint (nhds 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

theorem SeminormedAddGroup.disjoint_nhds_zero {E : Type u_4} [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_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[reducible, inline]

abbrev NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_4) (F : Type u_5) [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.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem dist_eq_norm_div {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

dist a b = ‖a / b‖

theorem dist_eq_norm_sub {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

dist a b = ‖a - b‖

theorem dist_eq_norm_div' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

dist a b = ‖b / a‖

theorem dist_eq_norm_sub' {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

dist a b = ‖b - a‖

theorem dist_eq_norm {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

dist a b = ‖a - b‖

Alias of dist_eq_norm_sub.

theorem dist_eq_norm' {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

dist a b = ‖b - a‖

Alias of dist_eq_norm_sub'.

theorem norm_inv_mul {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

‖a⁻¹ * b‖ = ‖a / b‖

theorem norm_neg_add {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

‖-a + b‖ = ‖a - b‖

theorem abs_norm_sub_norm_le' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

|‖a‖ - ‖b‖| ≤ ‖a / b‖

theorem abs_norm_sub_norm_le {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

|‖a‖ - ‖b‖| ≤ ‖a - b‖

theorem norm_sub_norm_le' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖a / b‖

theorem norm_sub_norm_le {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

‖a‖ - ‖b‖ ≤ ‖a - b‖

theorem dist_norm_norm_le' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

dist ‖a‖ ‖b‖ ≤ ‖a / b‖

theorem dist_norm_norm_le {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

dist ‖a‖ ‖b‖ ≤ ‖a - b‖

theorem nnDist_nnNorm_nnNorm_le' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

theorem nnDist_nnNorm_nnNorm_le {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊

@[deprecated nnDist_nnNorm_nnNorm_le' (since := "2026-10-31")]

theorem nndist_nnnorm_nnnorm_le' {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

Alias of nnDist_nnNorm_nnNorm_le'.

@[deprecated nnDist_nnNorm_nnNorm_le (since := "2026-10-31")]

theorem nndist_nnnorm_nnnorm_le {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊

Alias of nnDist_nnNorm_nnNorm_le.

theorem nnDist_eq_nnNorm_div {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

nndist a b = ‖a / b‖₊

theorem nnDist_eq_nnNorm_sub {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist a b = ‖a - b‖₊

@[deprecated nnDist_eq_nnNorm_div (since := "2026-10-31")]

theorem nndist_eq_nnnorm_div {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

nndist a b = ‖a / b‖₊

Alias of nnDist_eq_nnNorm_div.

@[deprecated nnDist_eq_nnNorm_sub (since := "2026-10-31")]

theorem nndist_eq_nnnorm_sub {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist a b = ‖a - b‖₊

Alias of nnDist_eq_nnNorm_sub.

theorem nnDist_eq_nnNorm {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist a b = ‖a - b‖₊

Alias of nnDist_eq_nnNorm_sub.

@[deprecated nnDist_eq_nnNorm (since := "2026-10-31")]

theorem nndist_eq_nnnorm {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

nndist a b = ‖a - b‖₊

Alias of nnDist_eq_nnNorm.

Alias of nnDist_eq_nnNorm_sub.

theorem edist_eq_enorm_div {E : Type u_4} [SeminormedCommGroup E] (a b : E) :

edist a b = ‖a / b‖ₑ

theorem edist_eq_enorm_sub {E : Type u_4} [SeminormedAddCommGroup E] (a b : E) :

edist a b = ‖a - b‖ₑ

theorem dist_inv {E : Type u_4} [SeminormedCommGroup E] (x y : E) :

dist x⁻¹ y = dist x y⁻¹

theorem dist_neg {E : Type u_4} [SeminormedAddCommGroup E] (x y : E) :

dist (-x) y = dist x (-y)

theorem norm_multiset_sum_le {E : Type u_8} [SeminormedAddCommGroup E] (m : Multiset E) :

‖m.sum‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem enorm_multisetSum_le {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] (m : Multiset ε) :

‖m.sum‖ₑ ≤ (Multiset.map (fun (x : ε) => ‖x‖ₑ) m).sum

theorem norm_multiset_prod_le {E : Type u_4} [SeminormedCommGroup E] (m : Multiset E) :

‖m.prod‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem enorm_multisetProd_le {ε : Type u_8} [TopologicalSpace ε] [ESeminormedCommMonoid ε] (m : Multiset ε) :

‖m.prod‖ₑ ≤ (Multiset.map (fun (x : ε) => ‖x‖ₑ) m).sum

theorem enorm_sum_le {ι : Type u_3} {ε : Type u_8} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] (s : Finset ι) (f : ι → ε) :

‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem norm_sum_le {ι : Type u_3} {E : Type u_8} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) :

‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

theorem enorm_prod_le {ι : Type u_3} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedCommMonoid ε] (s : Finset ι) (f : ι → ε) :

‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ

theorem norm_prod_le {ι : Type u_3} {E : Type u_4} [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_7} [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_7} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [SeminormedCommGroup E] (y : E) (ε : ℝ) :

Metric.ball y ε = {x : E | ‖x / y‖ < ε}

theorem ball_eq {E : Type u_4} [SeminormedAddCommGroup E] (y : E) (ε : ℝ) :

Metric.ball y ε = {x : E | ‖x - y‖ < ε}

theorem mem_ball_iff_norm'' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.ball a r ↔ ‖b / a‖ < r

theorem mem_ball_iff_norm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.ball a r ↔ ‖b - a‖ < r

theorem mem_ball_iff_norm''' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.ball a r ↔ ‖a / b‖ < r

theorem mem_ball_iff_norm' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.ball a r ↔ ‖a - b‖ < r

theorem setOf_div_mem_ball_eq_ball'' {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} :

{x : E | x / a ∈ Metric.ball 1 r} = Metric.ball a r

A scaled ball is a ball.

theorem setOf_sub_mem_ball_eq_ball {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} :

{x : E | x - a ∈ Metric.ball 0 r} = Metric.ball a r

A translated ball is a ball.

theorem mem_closedBall_iff_norm'' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r

theorem mem_closedBall_iff_norm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r

theorem mem_closedBall_iff_norm''' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r

theorem mem_closedBall_iff_norm' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r

theorem mem_closedBall_iff_nnNorm'' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖b / a‖₊ ≤ r

theorem mem_closedBall_iff_nnNorm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖b - a‖₊ ≤ r

@[deprecated mem_closedBall_iff_nnNorm'' (since := "2026-10-31")]

theorem mem_closedBall_iff_nnnorm'' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖b / a‖₊ ≤ r

Alias of mem_closedBall_iff_nnNorm''.

@[deprecated mem_closedBall_iff_nnNorm (since := "2026-10-31")]

theorem mem_closedBall_iff_nnnorm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖b - a‖₊ ≤ r

Alias of mem_closedBall_iff_nnNorm.

theorem mem_closedBall_iff_nnNorm''' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖a / b‖₊ ≤ r

theorem mem_closedBall_iff_nnNorm' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖a - b‖₊ ≤ r

@[deprecated mem_closedBall_iff_nnNorm''' (since := "2026-10-31")]

theorem mem_closedBall_iff_nnnorm''' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖a / b‖₊ ≤ r

Alias of mem_closedBall_iff_nnNorm'''.

@[deprecated mem_closedBall_iff_nnNorm' (since := "2026-10-31")]

theorem mem_closedBall_iff_nnnorm' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : NNReal} :

b ∈ Metric.closedBall a ↑r ↔ ‖a - b‖₊ ≤ r

Alias of mem_closedBall_iff_nnNorm'.

theorem setOf_div_mem_closedBall_eq_closedBall'' {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} :

{x : E | x / a ∈ Metric.closedBall 1 r} = Metric.closedBall a r

A scaled closed ball is a closed ball.

theorem setOf_sub_mem_closedBall_eq_closedBall {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} :

{x : E | x - a ∈ Metric.closedBall 0 r} = Metric.closedBall a r

A translated closed ball is a closed ball.

@[simp]

theorem mem_sphere_iff_norm' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.sphere a r ↔ ‖b / a‖ = r

@[simp]

theorem mem_sphere_iff_norm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

b ∈ Metric.sphere a r ↔ ‖b - a‖ = r

theorem setOf_div_mem_sphere_eq_sphere'' {E : Type u_4} [SeminormedCommGroup E] {a : E} {r : ℝ} :

{x : E | x / a ∈ Metric.sphere 1 r} = Metric.sphere a r

A scaled sphere is a sphere.

theorem setOf_sub_mem_sphere_eq_sphere {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {r : ℝ} :

{x : E | x - a ∈ Metric.sphere 0 r} = Metric.sphere a r

A translated sphere is a sphere.

theorem mul_mem_ball_iff_norm {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

a * b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem add_mem_ball_iff_norm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

a + b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem mul_mem_closedBall_iff_norm {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

theorem add_mem_closedBall_iff_norm {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

@[simp]

theorem preimage_mul_ball {E : Type u_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

a • Metric.closedBall b r = Metric.closedBall (a • b) r

theorem vadd_closedBall'' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r

theorem smul_ball'' {E : Type u_4} [SeminormedCommGroup E] {a b : E} {r : ℝ} :

a • Metric.ball b r = Metric.ball (a • b) r

theorem vadd_ball'' {E : Type u_4} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} :

a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r

theorem nnNorm_multiset_prod_le {E : Type u_4} [SeminormedCommGroup E] (m : Multiset E) :

‖m.prod‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

theorem nnNorm_multiset_sum_le {E : Type u_4} [SeminormedAddCommGroup E] (m : Multiset E) :

‖m.sum‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

@[deprecated nnNorm_multiset_prod_le (since := "2026-10-31")]

theorem nnnorm_multiset_prod_le {E : Type u_4} [SeminormedCommGroup E] (m : Multiset E) :

‖m.prod‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

Alias of nnNorm_multiset_prod_le.

@[deprecated nnNorm_multiset_sum_le (since := "2026-10-31")]

theorem nnnorm_multiset_sum_le {E : Type u_4} [SeminormedAddCommGroup E] (m : Multiset E) :

‖m.sum‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

Alias of nnNorm_multiset_sum_le.

theorem nnNorm_prod_le {ι : Type u_3} {E : Type u_4} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) :

‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

theorem nnNorm_sum_le {ι : Type u_3} {E : Type u_4} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) :

‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

@[deprecated nnNorm_prod_le (since := "2026-10-31")]

theorem nnnorm_prod_le {ι : Type u_3} {E : Type u_4} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) :

‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

Alias of nnNorm_prod_le.

@[deprecated nnNorm_sum_le (since := "2026-10-31")]

theorem nnnorm_sum_le {ι : Type u_3} {E : Type u_4} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) :

‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

Alias of nnNorm_sum_le.

theorem nnNorm_prod_le_of_le {ι : Type u_3} {E : Type u_4} [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_4} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) :

‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

@[deprecated nnNorm_prod_le_of_le (since := "2026-10-31")]

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

‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

Alias of nnNorm_prod_le_of_le.

@[deprecated nnNorm_sum_le_of_le (since := "2026-10-31")]

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

‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

Alias of nnNorm_sum_le_of_le.

theorem NormedCommGroup.tendsto_nhds_nhds {E : Type u_4} {F : Type u_5} [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_4} {F : Type u_5} [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_4} [SeminormedCommGroup E] (x : E) :

(nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y / x‖ < ε}

theorem NormedAddCommGroup.nhds_basis_norm_lt {E : Type u_4} [SeminormedAddCommGroup E] (x : E) :

(nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y - x‖ < ε}

theorem NormedCommGroup.uniformity_basis_dist {E : Type u_4} [SeminormedCommGroup E] :

(uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 / p.2‖ < ε}

theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_4} [SeminormedAddCommGroup E] :

(uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 - p.2‖ < ε}

@[simp]

theorem norm_le_zero_iff' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖ ≤ 0 ↔ a = 1

@[simp]

theorem norm_le_zero_iff {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖ ≤ 0 ↔ a = 0

@[simp]

theorem norm_pos_iff' {E : Type u_4} [NormedGroup E] {a : E} :

0 < ‖a‖ ↔ a ≠ 1

@[simp]

theorem norm_pos_iff {E : Type u_4} [NormedAddGroup E] {a : E} :

0 < ‖a‖ ↔ a ≠ 0

@[simp]

theorem norm_eq_zero' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖ = 0 ↔ a = 1

@[simp]

theorem norm_eq_zero {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖ = 0 ↔ a = 0

theorem norm_ne_zero_iff' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖ ≠ 0 ↔ a ≠ 1

theorem norm_ne_zero_iff {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖ ≠ 0 ↔ a ≠ 0

theorem norm_div_eq_zero_iff {E : Type u_4} [NormedGroup E] {a b : E} :

‖a / b‖ = 0 ↔ a = b

theorem norm_sub_eq_zero_iff {E : Type u_4} [NormedAddGroup E] {a b : E} :

‖a - b‖ = 0 ↔ a = b

theorem norm_div_pos_iff {E : Type u_4} [NormedGroup E] {a b : E} :

0 < ‖a / b‖ ↔ a ≠ b

theorem norm_sub_pos_iff {E : Type u_4} [NormedAddGroup E] {a b : E} :

0 < ‖a - b‖ ↔ a ≠ b

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

a = b

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

a = b

theorem eq_of_norm_div_eq_zero {E : Type u_4} [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_4} [NormedAddGroup E] {a b : E} :

‖a - b‖ = 0 → a = b

Alias of the forward direction of norm_sub_eq_zero_iff.

theorem eq_one_or_norm_pos {E : Type u_4} [NormedGroup E] (a : E) :

a = 1 ∨ 0 < ‖a‖

theorem eq_zero_or_norm_pos {E : Type u_4} [NormedAddGroup E] (a : E) :

a = 0 ∨ 0 < ‖a‖

theorem eq_one_or_nnNorm_pos {E : Type u_4} [NormedGroup E] (a : E) :

a = 1 ∨ 0 < ‖a‖₊

theorem eq_zero_or_nnNorm_pos {E : Type u_4} [NormedAddGroup E] (a : E) :

a = 0 ∨ 0 < ‖a‖₊

@[deprecated eq_one_or_nnNorm_pos (since := "2026-10-31")]

theorem eq_one_or_nnnorm_pos {E : Type u_4} [NormedGroup E] (a : E) :

a = 1 ∨ 0 < ‖a‖₊

Alias of eq_one_or_nnNorm_pos.

@[deprecated eq_zero_or_nnNorm_pos (since := "2026-10-31")]

theorem eq_zero_or_nnnorm_pos {E : Type u_4} [NormedAddGroup E] (a : E) :

a = 0 ∨ 0 < ‖a‖₊

Alias of eq_zero_or_nnNorm_pos.

@[simp]

theorem nnNorm_eq_zero' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖₊ = 0 ↔ a = 1

@[simp]

theorem nnNorm_eq_zero {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖₊ = 0 ↔ a = 0

@[deprecated nnNorm_eq_zero' (since := "2026-10-31")]

theorem nnnorm_eq_zero' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖₊ = 0 ↔ a = 1

Alias of nnNorm_eq_zero'.

@[deprecated nnNorm_eq_zero (since := "2026-10-31")]

theorem nnnorm_eq_zero {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖₊ = 0 ↔ a = 0

Alias of nnNorm_eq_zero.

theorem nnNorm_ne_zero_iff' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖₊ ≠ 0 ↔ a ≠ 1

theorem nnNorm_ne_zero_iff {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖₊ ≠ 0 ↔ a ≠ 0

@[deprecated nnNorm_ne_zero_iff' (since := "2026-10-31")]

theorem nnnorm_ne_zero_iff' {E : Type u_4} [NormedGroup E] {a : E} :

‖a‖₊ ≠ 0 ↔ a ≠ 1

Alias of nnNorm_ne_zero_iff'.

@[deprecated nnNorm_ne_zero_iff (since := "2026-10-31")]

theorem nnnorm_ne_zero_iff {E : Type u_4} [NormedAddGroup E] {a : E} :

‖a‖₊ ≠ 0 ↔ a ≠ 0

Alias of nnNorm_ne_zero_iff.

@[simp]

theorem nnNorm_pos' {E : Type u_4} [NormedGroup E] {a : E} :

0 < ‖a‖₊ ↔ a ≠ 1

@[simp]

theorem nnNorm_pos {E : Type u_4} [NormedAddGroup E] {a : E} :

0 < ‖a‖₊ ↔ a ≠ 0

@[deprecated nnNorm_pos' (since := "2026-10-31")]

theorem nnnorm_pos' {E : Type u_4} [NormedGroup E] {a : E} :

0 < ‖a‖₊ ↔ a ≠ 1

Alias of nnNorm_pos'.

@[deprecated nnNorm_pos (since := "2026-10-31")]

theorem nnnorm_pos {E : Type u_4} [NormedAddGroup E] {a : E} :

0 < ‖a‖₊ ↔ a ≠ 0

Alias of nnNorm_pos.

def normGroupNorm (E : Type u_4) [NormedGroup E] :

GroupNorm E

The norm of a normed group as a group norm.

Equations

normGroupNorm E = { toGroupSeminorm := normGroupSeminorm E, eq_one_of_map_eq_zero' := ⋯ }

Instances For

def normAddGroupNorm (E : Type u_4) [NormedAddGroup E] :

AddGroupNorm E

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

Equations

normAddGroupNorm E = { toAddGroupSeminorm := normAddGroupSeminorm E, eq_zero_of_map_eq_zero' := ⋯ }

Instances For

@[simp]

theorem coe_normGroupNorm (E : Type u_4) [NormedGroup E] :

⇑(normGroupNorm E) = norm

Some relations with HasCompactSupport

theorem hasCompactSupport_norm_iff {α : Type u_2} {E : Type u_4} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} :

(HasCompactSupport fun (x : α) => ‖f x‖) ↔ HasCompactSupport f

theorem HasCompactSupport.norm {α : Type u_2} {E : Type u_4} [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.

Instances For