Mathlib.Topology.Algebra.Monoid

continuous_one theorem

[TopologicalSpace M] [One M] : Continuous (1 : X → M)

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_one [TopologicalSpace M] [One M] : Continuous (1 : X → M) :=
  @continuous_const _ _ _ _ 1

Continuity of the Constant One Function

Informal description

Let $M$ be a topological space equipped with a distinguished element $1$ (i.e., a `One` instance). Then the constant function $1 : X \to M$ is continuous.

instContinuousMulOrderDual instance

: ContinuousMul Mᵒᵈ

Full source

@[to_additive]
instance : ContinuousMul Mᵒᵈ :=
  ‹ContinuousMul M›

Continuous Multiplication on Order Dual

Informal description

For any type $M$ with a continuous multiplication operation, the order dual $M^{\text{op}}$ also has a continuous multiplication operation.

instContinuousMulULift instance

: ContinuousMul (ULift.{u} M)

Full source

@[to_additive]
instance : ContinuousMul (ULift.{u} M) := by
  constructor
  apply continuous_uliftUp.comp
  exact continuous_mul.comp₂ (continuous_uliftDown.comp continuous_fst)
    (continuous_uliftDown.comp continuous_snd)

Continuous Multiplication on Lifted Types

Informal description

For any type $M$ with a continuous multiplication operation, the lifted type $\mathrm{ULift}\,M$ also has a continuous multiplication operation.

ContinuousMul.to_continuousSMul instance

: ContinuousSMul M M

Full source

@[to_additive]
instance ContinuousMul.to_continuousSMul : ContinuousSMul M M :=
  ⟨continuous_mul⟩

Continuous Scalar Multiplication in Topological Monoids

Informal description

For any topological monoid $M$ with continuous multiplication, the scalar multiplication operation $M \times M \to M$ is continuous.

ContinuousMul.to_continuousSMul_op instance

: ContinuousSMul Mᵐᵒᵖ M

Full source

@[to_additive]
instance ContinuousMul.to_continuousSMul_op : ContinuousSMul Mᵐᵒᵖ M :=
  ⟨show Continuous ((fun p : M × M => p.1 * p.2) ∘ Prod.swap ∘ Prod.map MulOpposite.unop id) from
      continuous_mul.comp <|
        continuous_swap.comp <| Continuous.prodMap MulOpposite.continuous_unop continuous_id⟩

Continuous Scalar Multiplication from Opposite Monoid

Informal description

For any topological monoid $M$ with continuous multiplication, the scalar multiplication operation from the opposite monoid $M^{\text{op}}$ to $M$ is continuous.

ContinuousMul.induced theorem

 {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Mul α] [Mul β] [MulHomClass F α β] [tβ : TopologicalSpace β]
  [ContinuousMul β] (f : F) : @ContinuousMul α (tβ.induced f) _

Full source

@[to_additive]
theorem ContinuousMul.induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Mul α]
    [Mul β] [MulHomClass F α β] [tβ : TopologicalSpace β] [ContinuousMul β] (f : F) :
    @ContinuousMul α (tβ.induced f) _ := by
  let tα := tβ.induced f
  refine ⟨continuous_induced_rng.2 ?_⟩
  simp only [Function.comp_def, map_mul]
  fun_prop

Induced Topology Preserves Continuous Multiplication via Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types with multiplication operations, and let $F$ be a type of functions from $\alpha$ to $\beta$ that preserve multiplication. Suppose $\beta$ is equipped with a topology making multiplication continuous. Given a function $f \in F$, the topology on $\alpha$ induced by $f$ makes multiplication on $\alpha$ continuous.

continuous_mul_left theorem

(a : M) : Continuous fun b : M => a * b

Full source

@[to_additive (attr := continuity)]
theorem continuous_mul_left (a : M) : Continuous fun b : M => a * b :=
  continuous_const.mul continuous_id

Left Multiplication is Continuous in Topological Monoids

Informal description

For any element $a$ in a topological monoid $M$, the function $b \mapsto a * b$ is continuous.

continuous_mul_right theorem

(a : M) : Continuous fun b : M => b * a

Full source

@[to_additive (attr := continuity)]
theorem continuous_mul_right (a : M) : Continuous fun b : M => b * a :=
  continuous_id.mul continuous_const

Continuity of Right Multiplication in Topological Monoids

Informal description

For any element $a$ in a topological monoid $M$, the right multiplication map $b \mapsto b * a$ is continuous.

tendsto_mul theorem

{a b : M} : Tendsto (fun p : M × M => p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b))

Full source

@[to_additive]
theorem tendsto_mul {a b : M} : Tendsto (fun p : M × M => p.fst * p.snd) (𝓝 (a, b)) (𝓝 (a * b)) :=
  continuous_iff_continuousAt.mp ContinuousMul.continuous_mul (a, b)

Continuity of Multiplication in Topological Monoids

Informal description

For any elements $a, b$ in a topological monoid $M$, the multiplication operation $(x, y) \mapsto x * y$ is continuous at $(a, b)$. That is, the limit of $x_n * y_n$ as $(x_n, y_n)$ approaches $(a, b)$ is $a * b$.

Filter.Tendsto.const_mul theorem

 (b : M) {c : M} {f : α → M} {l : Filter α} (h : Tendsto (fun k : α => f k) l (𝓝 c)) :
  Tendsto (fun k : α => b * f k) l (𝓝 (b * c))

Full source

@[to_additive]
theorem Filter.Tendsto.const_mul (b : M) {c : M} {f : α → M} {l : Filter α}
    (h : Tendsto (fun k : α => f k) l (𝓝 c)) : Tendsto (fun k : α => b * f k) l (𝓝 (b * c)) :=
  tendsto_const_nhds.mul h

Continuity of left multiplication in topological monoids

Informal description

Let $M$ be a topological space with a continuous multiplication operation. For any fixed element $b \in M$, if a function $f : \alpha \to M$ tends to $c \in M$ along a filter $l$ on $\alpha$, then the function $k \mapsto b \cdot f(k)$ tends to $b \cdot c$ along the same filter $l$.

Filter.Tendsto.mul_const theorem

 (b : M) {c : M} {f : α → M} {l : Filter α} (h : Tendsto (fun k : α => f k) l (𝓝 c)) :
  Tendsto (fun k : α => f k * b) l (𝓝 (c * b))

Full source

@[to_additive]
theorem Filter.Tendsto.mul_const (b : M) {c : M} {f : α → M} {l : Filter α}
    (h : Tendsto (fun k : α => f k) l (𝓝 c)) : Tendsto (fun k : α => f k * b) l (𝓝 (c * b)) :=
  h.mul tendsto_const_nhds

Right Multiplication Preserves Filter Limits in Topological Monoids

Informal description

Let $M$ be a topological space with a multiplication operation, and let $f : \alpha \to M$ be a function. If $f$ tends to $c \in M$ along a filter $l$ on $\alpha$, then for any $b \in M$, the function $k \mapsto f(k) * b$ tends to $c * b$ along $l$.

le_nhds_mul theorem

(a b : M) : 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)

Full source

@[to_additive]
theorem le_nhds_mul (a b : M) : 𝓝 a * 𝓝 b ≤ 𝓝 (a * b) := by
  rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
  exact continuous_mul.tendsto _

Neighborhood Product is Contained in Product Neighborhood in Topological Monoids

Informal description

For any elements $a$ and $b$ in a topological monoid $M$, the product of their neighborhoods $\mathcal{N}_a * \mathcal{N}_b$ is contained in the neighborhood of their product $\mathcal{N}_{a * b}$.

nhds_one_mul_nhds theorem

{M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : 𝓝 (1 : M) * 𝓝 a = 𝓝 a

Full source

@[to_additive (attr := simp)]
theorem nhds_one_mul_nhds {M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) :
    𝓝 (1 : M) * 𝓝 a = 𝓝 a :=
  ((le_nhds_mul _ _).trans_eq <| congr_arg _ (one_mul a)).antisymm <|
    le_mul_of_one_le_left' <| pure_le_nhds 1

Neighborhood of Identity Multiplied by Neighborhood of Element Equals Neighborhood of Element in Topological Monoid

Informal description

Let $M$ be a topological monoid with a multiplicative identity element $1$ and continuous multiplication. For any element $a \in M$, the product of the neighborhood of $1$ and the neighborhood of $a$ is equal to the neighborhood of $a$, i.e., $\mathcal{N}_1 * \mathcal{N}_a = \mathcal{N}_a$.

nhds_mul_nhds_one theorem

{M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : 𝓝 a * 𝓝 1 = 𝓝 a

Full source

@[to_additive (attr := simp)]
theorem nhds_mul_nhds_one {M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) :
    𝓝 a * 𝓝 1 = 𝓝 a :=
  ((le_nhds_mul _ _).trans_eq <| congr_arg _ (mul_one a)).antisymm <|
    le_mul_of_one_le_right' <| pure_le_nhds 1

Neighborhood Product with Identity Equals Original Neighborhood in Topological Monoids

Informal description

For any element $a$ in a topological monoid $M$ with multiplicative identity $1$, the product of the neighborhood of $a$ and the neighborhood of $1$ is equal to the neighborhood of $a$, i.e., $\mathcal{N}_a * \mathcal{N}_1 = \mathcal{N}_a$.

Filter.TendstoNhdsWithinIoi.const_mul theorem

 [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜] (h : Tendsto f l (𝓝[>] c)) : Tendsto (fun a => b * f a) l (𝓝[>] (b * c))

Full source

theorem Filter.TendstoNhdsWithinIoi.const_mul [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜]
    (h : Tendsto f l (𝓝[>] c)) : Tendsto (fun a => b * f a) l (𝓝[>] (b * c)) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      ((tendsto_nhds_of_tendsto_nhdsWithin h).const_mul b) <|
    (tendsto_nhdsWithin_iff.mp h).2.mono fun _ => (mul_lt_mul_left hb).mpr

Right-neighborhood limit preservation under left multiplication by positive elements: $f \to_{>c} c \implies b \cdot f \to_{>b \cdot c} b \cdot c$

Informal description

Let $\mathbb{K}$ be a preordered type with a multiplication operation such that left multiplication by positive elements is strictly monotone (`PosMulStrictMono 𝕜`) and reflects the strict order (`PosMulReflectLT 𝕜`). Given a function $f : \alpha \to \mathbb{K}$ that tends to $c$ within the right-neighborhood $\mathcal{N}_{>c}$ along a filter $l$, then for any fixed element $b \in \mathbb{K}$, the function $a \mapsto b \cdot f(a)$ tends to $b \cdot c$ within the right-neighborhood $\mathcal{N}_{>b \cdot c}$ along the same filter $l$.

Filter.TendstoNhdsWithinIio.const_mul theorem

 [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜] (h : Tendsto f l (𝓝[<] c)) : Tendsto (fun a => b * f a) l (𝓝[<] (b * c))

Full source

theorem Filter.TendstoNhdsWithinIio.const_mul [PosMulStrictMono 𝕜] [PosMulReflectLT 𝕜]
    (h : Tendsto f l (𝓝[<] c)) : Tendsto (fun a => b * f a) l (𝓝[<] (b * c)) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      ((tendsto_nhds_of_tendsto_nhdsWithin h).const_mul b) <|
    (tendsto_nhdsWithin_iff.mp h).2.mono fun _ => (mul_lt_mul_left hb).mpr

Left-neighborhood limit preservation under left multiplication by positive elements: $f \to_{

Informal description

Let $\mathbb{K}$ be a preordered type with a multiplication operation such that left multiplication by positive elements is strictly monotone (`PosMulStrictMono 𝕜`) and reflects the strict order (`PosMulReflectLT 𝕜`). Given a function $f : \alpha \to \mathbb{K}$ that tends to $c$ within the left-neighborhood $\mathcal{N}_{

Filter.TendstoNhdsWithinIoi.mul_const theorem

 [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜] (h : Tendsto f l (𝓝[>] c)) : Tendsto (fun a => f a * b) l (𝓝[>] (c * b))

Full source

theorem Filter.TendstoNhdsWithinIoi.mul_const [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜]
    (h : Tendsto f l (𝓝[>] c)) : Tendsto (fun a => f a * b) l (𝓝[>] (c * b)) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      ((tendsto_nhds_of_tendsto_nhdsWithin h).mul_const b) <|
    (tendsto_nhdsWithin_iff.mp h).2.mono fun _ => (mul_lt_mul_right hb).mpr

Right-neighborhood limit preservation under right multiplication by positive elements: $f \to_{>c} c \implies f \cdot b \to_{>c \cdot b} c \cdot b$

Informal description

Let $\mathbb{K}$ be a preordered type with a multiplication operation such that right multiplication by positive elements is strictly monotone (`MulPosStrictMono 𝕜`) and reflects the strict order (`MulPosReflectLT 𝕜`). Given a function $f : \alpha \to \mathbb{K}$ that tends to $c$ within the right-neighborhood $\mathcal{N}_{>c}$ along a filter $l$, then for any fixed element $b \in \mathbb{K}$, the function $a \mapsto f(a) \cdot b$ tends to $c \cdot b$ within the right-neighborhood $\mathcal{N}_{>c \cdot b}$ along the same filter $l$.

Filter.TendstoNhdsWithinIio.mul_const theorem

 [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜] (h : Tendsto f l (𝓝[<] c)) : Tendsto (fun a => f a * b) l (𝓝[<] (c * b))

Full source

theorem Filter.TendstoNhdsWithinIio.mul_const [MulPosStrictMono 𝕜] [MulPosReflectLT 𝕜]
    (h : Tendsto f l (𝓝[<] c)) : Tendsto (fun a => f a * b) l (𝓝[<] (c * b)) :=
  tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      ((tendsto_nhds_of_tendsto_nhdsWithin h).mul_const b) <|
    (tendsto_nhdsWithin_iff.mp h).2.mono fun _ => (mul_lt_mul_right hb).mpr

Left-neighborhood limit preservation under right multiplication by positive elements: $f \to_{

Informal description

Let $\mathbb{K}$ be a preordered type with a multiplication operation such that right multiplication by positive elements is strictly monotone and reflects the strict order. Given a function $f : \alpha \to \mathbb{K}$ that tends to $c$ within the left-neighborhood $\{x \mid x < c\}$ along a filter $l$, then for any fixed element $b \in \mathbb{K}$, the function $a \mapsto f(a) \cdot b$ tends to $c \cdot b$ within the left-neighborhood $\{x \mid x < c \cdot b\}$ along the same filter $l$.

Specializes.mul theorem

{a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) : (a * c) ⤳ (b * d)

Full source

@[to_additive]
protected theorem Specializes.mul {a b c d : M} (hab : a ⤳ b) (hcd : c ⤳ d) : (a * c) ⤳ (b * d) :=
  hab.smul hcd

Specialization is preserved under multiplication in topological monoids

Informal description

Let $M$ be a topological monoid with continuous multiplication. For any elements $a, b, c, d \in M$, if $a$ specializes to $b$ and $c$ specializes to $d$, then the product $a \cdot c$ specializes to $b \cdot d$.

Inseparable.mul theorem

{a b c d : M} (hab : Inseparable a b) (hcd : Inseparable c d) : Inseparable (a * c) (b * d)

Full source

@[to_additive]
protected theorem Inseparable.mul {a b c d : M} (hab : Inseparable a b) (hcd : Inseparable c d) :
    Inseparable (a * c) (b * d) :=
  hab.smul hcd

Inseparability is preserved under multiplication in topological monoids

Informal description

Let $M$ be a topological monoid with continuous multiplication. For any elements $a, b, c, d \in M$, if $a$ is inseparable from $b$ and $c$ is inseparable from $d$, then their products satisfy $a \cdot c$ is inseparable from $b \cdot d$.

Specializes.pow theorem

{M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : a ⤳ b) (n : ℕ) : (a ^ n) ⤳ (b ^ n)

Full source

@[to_additive]
protected theorem Specializes.pow {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M]
    {a b : M} (h : a ⤳ b) (n : ℕ) : (a ^ n) ⤳ (b ^ n) :=
  Nat.recOn n (by simp only [pow_zero, specializes_rfl]) fun _ ihn ↦ by
    simpa only [pow_succ] using ihn.mul h

Specialization is preserved under exponentiation in topological monoids

Informal description

Let $M$ be a topological monoid with continuous multiplication. For any elements $a, b \in M$ such that $a$ specializes to $b$, and for any natural number $n$, the $n$-th power $a^n$ specializes to $b^n$.

Inseparable.pow theorem

 {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] {a b : M} (h : Inseparable a b) (n : ℕ) :
  Inseparable (a ^ n) (b ^ n)

Full source

@[to_additive]
protected theorem Inseparable.pow {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M]
    {a b : M} (h : Inseparable a b) (n : ℕ) : Inseparable (a ^ n) (b ^ n) :=
  (h.specializes.pow n).antisymm (h.specializes'.pow n)

Inseparability is preserved under exponentiation in topological monoids

Informal description

Let $M$ be a topological monoid with continuous multiplication. For any elements $a, b \in M$ such that $a$ is inseparable from $b$, and for any natural number $n$, the $n$-th powers $a^n$ and $b^n$ are also inseparable.

Filter.Tendsto.units definition

 [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot]
  (h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁)) (h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)) : Nˣ

Full source

/-- Construct a unit from limits of units and their inverses. -/
@[to_additive (attr := simps)
  "Construct an additive unit from limits of additive units and their negatives."]
def Filter.Tendsto.units [TopologicalSpace N] [Monoid N] [ContinuousMul N] [T2Space N]
    {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [l.NeBot] (h₁ : Tendsto (fun x => ↑(f x)) l (𝓝 r₁))
    (h₂ : Tendsto (fun x => ↑(f x)⁻¹) l (𝓝 r₂)) : Nˣ where
  val := r₁
  inv := r₂
  val_inv := by
    symm
    simpa using h₁.mul h₂
  inv_val := by
    symm
    simpa using h₂.mul h₁

Construction of a unit from limits of units and their inverses

Informal description

Given a topological monoid $N$ with continuous multiplication and Hausdorff topology, and a filter $l$ over some index set $\iota$ that is not the trivial filter, suppose we have a function $f : \iota \to N^\times$ (where $N^\times$ denotes the units of $N$) such that: 1. The limit of $f(x)$ as $x$ tends along $l$ is $r_1$, 2. The limit of $f(x)^{-1}$ as $x$ tends along $l$ is $r_2$. Then we can construct a unit of $N$ with value $r_1$ and inverse $r_2$, where the product conditions $r_1 \cdot r_2 = 1$ and $r_2 \cdot r_1 = 1$ hold by the continuity of multiplication.

Prod.continuousMul instance

[TopologicalSpace N] [Mul N] [ContinuousMul N] : ContinuousMul (M × N)

Full source

@[to_additive]
instance Prod.continuousMul [TopologicalSpace N] [Mul N] [ContinuousMul N] :
    ContinuousMul (M × N) :=
  ⟨by apply Continuous.prodMk <;> fun_prop⟩

Continuous Multiplication on Product Spaces

Informal description

For any topological spaces $M$ and $N$ with multiplication operations and continuous multiplication, the product space $M \times N$ also has continuous multiplication.

Pi.continuousMul instance

 {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Mul (C i)] [∀ i, ContinuousMul (C i)] : ContinuousMul (∀ i, C i)

Full source

@[to_additive]
instance Pi.continuousMul {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Mul (C i)]
    [∀ i, ContinuousMul (C i)] : ContinuousMul (∀ i, C i) where
  continuous_mul :=
    continuous_pi fun i => (continuous_apply i).fst'.mul (continuous_apply i).snd'

Continuous Multiplication on Product Spaces

Informal description

For any family of types $\{C_i\}_{i \in \iota}$ where each $C_i$ is equipped with a topological space structure, a multiplication operation, and the property that multiplication is continuous, the product space $\prod_{i \in \iota} C_i$ also has the property that multiplication is continuous.

Pi.continuousMul' instance

: ContinuousMul (ι → M)

Full source

/-- A version of `Pi.continuousMul` for non-dependent functions. It is needed because sometimes
Lean 3 fails to use `Pi.continuousMul` for non-dependent functions. -/
@[to_additive "A version of `Pi.continuousAdd` for non-dependent functions. It is needed
because sometimes Lean fails to use `Pi.continuousAdd` for non-dependent functions."]
instance Pi.continuousMul' : ContinuousMul (ι → M) :=
  Pi.continuousMul

Continuous Multiplication on Function Spaces

Informal description

For any type $M$ with a multiplication operation and continuous multiplication, and any index type $\iota$, the function space $\iota \to M$ has continuous multiplication.

continuousMul_of_discreteTopology instance

[TopologicalSpace N] [Mul N] [DiscreteTopology N] : ContinuousMul N

Full source

@[to_additive]
instance (priority := 100) continuousMul_of_discreteTopology [TopologicalSpace N] [Mul N]
    [DiscreteTopology N] : ContinuousMul N :=
  ⟨continuous_of_discreteTopology⟩

Continuous Multiplication in Discrete Topological Spaces

Informal description

For any topological space $N$ with a multiplication operation and discrete topology, the multiplication operation is continuous.

ContinuousMul.of_nhds_one theorem

 {M : Type u} [Monoid M] [TopologicalSpace M] (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) <| 𝓝 1)
  (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) (hright : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) :
  ContinuousMul M

Full source

@[to_additive]
theorem ContinuousMul.of_nhds_one {M : Type u} [Monoid M] [TopologicalSpace M]
    (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) <| 𝓝 1)
    (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
    (hright : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : ContinuousMul M :=
  ⟨by
    rw [continuous_iff_continuousAt]
    rintro ⟨x₀, y₀⟩
    have key : (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) =
        ((fun x => x₀ * x) ∘ fun x => x * y₀) ∘ uncurry (· * ·) := by
      ext p
      simp [uncurry, mul_assoc]
    have key₂ : ((fun x => x₀ * x) ∘ fun x => y₀ * x) = fun x => x₀ * y₀ * x := by
      ext x
      simp [mul_assoc]
    calc
      map (uncurry (· * ·)) (𝓝 (x₀, y₀)) = map (uncurry (· * ·)) (𝓝 x₀ ×ˢ 𝓝 y₀) := by
        rw [nhds_prod_eq]
      _ = map (fun p : M × M => x₀ * p.1 * (p.2 * y₀)) (𝓝 1 ×ˢ 𝓝 1) := by
        -- Porting note: `rw` was able to prove this
        -- Now it fails with `failed to rewrite using equation theorems for 'Function.uncurry'`
        -- and `failed to rewrite using equation theorems for 'Function.comp'`.
        -- Removing those two lemmas, the `rw` would succeed, but then needs a `rfl`.
        simp +unfoldPartialApp only [uncurry]
        simp_rw [hleft x₀, hright y₀, prod_map_map_eq, Filter.map_map, Function.comp_def]
      _ = map ((fun x => x₀ * x) ∘ fun x => x * y₀) (map (uncurry (· * ·)) (𝓝 1 ×ˢ 𝓝 1)) := by
        rw [key, ← Filter.map_map]
      _ ≤ map ((fun x : M => x₀ * x) ∘ fun x => x * y₀) (𝓝 1) := map_mono hmul
      _ = 𝓝 (x₀ * y₀) := by
        rw [← Filter.map_map, ← hright, hleft y₀, Filter.map_map, key₂, ← hleft]⟩

Criterion for Continuous Multiplication via Neighborhoods of Identity

Informal description

Let $M$ be a monoid with a topological space structure. If the following conditions hold: 1. The multiplication operation $(x,y) \mapsto x * y$ is continuous at $(1,1)$, 2. For every $x_0 \in M$, the neighborhood filter $\mathcal{N}(x_0)$ equals the image of $\mathcal{N}(1)$ under the left multiplication map $x \mapsto x_0 * x$, 3. For every $x_0 \in M$, the neighborhood filter $\mathcal{N}(x_0)$ equals the image of $\mathcal{N}(1)$ under the right multiplication map $x \mapsto x * x_0$, then $M$ has a continuous multiplication operation (i.e., satisfies the `ContinuousMul` condition).

continuousMul_of_comm_of_nhds_one theorem

 (M : Type u) [CommMonoid M] [TopologicalSpace M] (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
  (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) : ContinuousMul M

Full source

@[to_additive]
theorem continuousMul_of_comm_of_nhds_one (M : Type u) [CommMonoid M] [TopologicalSpace M]
    (hmul : Tendsto (uncurry ((· * ·) : M → M → M)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : M, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)) : ContinuousMul M := by
  apply ContinuousMul.of_nhds_one hmul hleft
  intro x₀
  simp_rw [mul_comm, hleft x₀]

Continuous Multiplication Criterion for Commutative Monoids via Neighborhoods of Identity

Informal description

Let $M$ be a commutative monoid with a topological space structure. If the following conditions hold: 1. The multiplication operation $(x,y) \mapsto x \cdot y$ is continuous at $(1,1)$, and 2. For every $x_0 \in M$, the neighborhood filter $\mathcal{N}(x_0)$ equals the image of $\mathcal{N}(1)$ under the left multiplication map $x \mapsto x_0 \cdot x$, then $M$ has a continuous multiplication operation (i.e., satisfies the `ContinuousMul` condition).

isClosed_setOf_map_one theorem

[One M₁] [One M₂] : IsClosed {f : M₁ → M₂ | f 1 = 1}

Full source

@[to_additive]
theorem isClosed_setOf_map_one [One M₁] [One M₂] : IsClosed { f : M₁ → M₂ | f 1 = 1 } :=
  isClosed_eq (continuous_apply 1) continuous_const

Closedness of the set of functions preserving the unit element

Informal description

For any types $M₁$ and $M₂$ equipped with a distinguished element (denoted by `1`), the set of all functions $f \colon M₁ \to M₂$ satisfying $f(1) = 1$ is closed in the function space $M₁ \to M₂$ with respect to the topology of pointwise convergence.

isClosed_setOf_map_mul theorem

[Mul M₁] [Mul M₂] [ContinuousMul M₂] : IsClosed {f : M₁ → M₂ | ∀ x y, f (x * y) = f x * f y}

Full source

@[to_additive]
theorem isClosed_setOf_map_mul [Mul M₁] [Mul M₂] [ContinuousMul M₂] :
    IsClosed { f : M₁ → M₂ | ∀ x y, f (x * y) = f x * f y } := by
  simp only [setOf_forall]
  exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦
    isClosed_eq (continuous_apply _) (by fun_prop)

Closedness of Multiplicative Homomorphisms under Pointwise Convergence

Informal description

Let $M_1$ and $M_2$ be types equipped with multiplication operations, and suppose $M_2$ has a topology making multiplication continuous. Then the set of functions $\{f : M_1 \to M_2 \mid \forall x y \in M_1, f(x \cdot y) = f(x) \cdot f(y)\}$ is closed in the topology of pointwise convergence.

mulHomOfMemClosureRangeCoe definition

(f : M₁ → M₂) (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →ₙ* M₂

Full source

/-- Construct a bundled semigroup homomorphism `M₁ →ₙ* M₂` from a function `f` and a proof that it
belongs to the closure of the range of the coercion from `M₁ →ₙ* M₂` (or another type of bundled
homomorphisms that has a `MulHomClass` instance) to `M₁ → M₂`. -/
@[to_additive (attr := simps -fullyApplied)
  "Construct a bundled additive semigroup homomorphism `M₁ →ₙ+ M₂` from a function `f`
and a proof that it belongs to the closure of the range of the coercion from `M₁ →ₙ+ M₂` (or another
type of bundled homomorphisms that has an `AddHomClass` instance) to `M₁ → M₂`."]
def mulHomOfMemClosureRangeCoe (f : M₁ → M₂)
    (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →ₙ* M₂ where
  toFun := f
  map_mul' := (isClosed_setOf_map_mul M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_mul) hf

Bundled multiplicative homomorphism from closure of homomorphism range

Informal description

Given a function $f \colon M_1 \to M_2$ that lies in the closure of the range of the coercion from bundled multiplicative homomorphisms $F$ (or another type with a `MulHomClass` instance) to functions $M_1 \to M_2$, construct a bundled multiplicative homomorphism $M_1 \to_{\cdot} M_2$ with $f$ as its underlying function.

mulHomOfTendsto definition

(f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →ₙ* M₂

Full source

/-- Construct a bundled semigroup homomorphism from a pointwise limit of semigroup homomorphisms. -/
@[to_additive (attr := simps! -fullyApplied)
  "Construct a bundled additive semigroup homomorphism from a pointwise limit of additive
semigroup homomorphisms"]
def mulHomOfTendsto (f : M₁ → M₂) (g : α → F) [l.NeBot]
    (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →ₙ* M₂ :=
  mulHomOfMemClosureRangeCoe f <|
    mem_closure_of_tendsto h <| Eventually.of_forall fun _ => mem_range_self _

Multiplicative homomorphism from limit of homomorphisms

Informal description

Given a function $f \colon M_1 \to M_2$, a filter $l$ on some type $\alpha$ that is not the trivial filter, and a family of functions $g \colon \alpha \to F$ (where $F$ is a type of multiplicative homomorphisms) such that the pointwise limit of $g$ tends to $f$ under $l$, then $f$ is a multiplicative homomorphism from $M_1$ to $M_2$.

MulHom.isClosed_range_coe theorem

: IsClosed (Set.range ((↑) : (M₁ →ₙ* M₂) → M₁ → M₂))

Full source

@[to_additive]
theorem MulHom.isClosed_range_coe : IsClosed (Set.range ((↑) : (M₁ →ₙ* M₂) → M₁ → M₂)) :=
  isClosed_of_closure_subset fun f hf => ⟨mulHomOfMemClosureRangeCoe f hf, rfl⟩

Closedness of Multiplicative Homomorphism Range in Function Space

Informal description

The range of the canonical embedding from the set of multiplicative homomorphisms $M_1 \to_{\cdot} M_2$ to the set of functions $M_1 \to M_2$ is closed in the function space topology.

monoidHomOfMemClosureRangeCoe definition

(f : M₁ → M₂) (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →* M₂

Full source

/-- Construct a bundled monoid homomorphism `M₁ →* M₂` from a function `f` and a proof that it
belongs to the closure of the range of the coercion from `M₁ →* M₂` (or another type of bundled
homomorphisms that has a `MonoidHomClass` instance) to `M₁ → M₂`. -/
@[to_additive (attr := simps -fullyApplied)
  "Construct a bundled additive monoid homomorphism `M₁ →+ M₂` from a function `f`
and a proof that it belongs to the closure of the range of the coercion from `M₁ →+ M₂` (or another
type of bundled homomorphisms that has an `AddMonoidHomClass` instance) to `M₁ → M₂`."]
def monoidHomOfMemClosureRangeCoe (f : M₁ → M₂)
    (hf : f ∈ closure (range fun (f : F) (x : M₁) => f x)) : M₁ →* M₂ where
  toFun := f
  map_one' := (isClosed_setOf_map_one M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_one) hf
  map_mul' := (isClosed_setOf_map_mul M₁ M₂).closure_subset_iff.2 (range_subset_iff.2 map_mul) hf

Monoid homomorphism from closure of homomorphism range

Informal description

Given a function $ f : M_1 \to M_2 $ that lies in the closure of the range of the coercion from bundled monoid homomorphisms $ M_1 \to* M_2 $ (or another type of bundled homomorphisms with a `MonoidHomClass` instance) to functions $ M_1 \to M_2 $, this constructs a bundled monoid homomorphism $ M_1 \to* M_2 $ from $ f $. The constructed homomorphism preserves the multiplicative identity and the multiplication operation.

monoidHomOfTendsto definition

(f : M₁ → M₂) (g : α → F) [l.NeBot] (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →* M₂

Full source

/-- Construct a bundled monoid homomorphism from a pointwise limit of monoid homomorphisms. -/
@[to_additive (attr := simps! -fullyApplied)
  "Construct a bundled additive monoid homomorphism from a pointwise limit of additive
monoid homomorphisms"]
def monoidHomOfTendsto (f : M₁ → M₂) (g : α → F) [l.NeBot]
    (h : Tendsto (fun a x => g a x) l (𝓝 f)) : M₁ →* M₂ :=
  monoidHomOfMemClosureRangeCoe f <|
    mem_closure_of_tendsto h <| Eventually.of_forall fun _ => mem_range_self _

Monoid homomorphism from pointwise limit of homomorphisms

Informal description

Given a function $ f : M_1 \to M_2 $ and a net $ g : \alpha \to F $ (where $ F $ is a type of bundled monoid homomorphisms) that converges pointwise to $ f $, this constructs a bundled monoid homomorphism $ M_1 \to* M_2 $ from $ f $. The constructed homomorphism preserves the multiplicative identity and the multiplication operation.

MonoidHom.isClosed_range_coe theorem

: IsClosed (Set.range ((↑) : (M₁ →* M₂) → M₁ → M₂))

Full source

@[to_additive]
theorem MonoidHom.isClosed_range_coe : IsClosed (Set.range ((↑) : (M₁ →* M₂) → M₁ → M₂)) :=
  isClosed_of_closure_subset fun f hf => ⟨monoidHomOfMemClosureRangeCoe f hf, rfl⟩

Closedness of Monoid Homomorphism Embedding Range

Informal description

The range of the canonical embedding from the space of monoid homomorphisms $M_1 \to* M_2$ to the space of functions $M_1 \to M_2$ is closed in the function space topology.

Topology.IsInducing.continuousMul theorem

 {M N F : Type*} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace M] [TopologicalSpace N]
  [ContinuousMul N] (f : F) (hf : IsInducing f) : ContinuousMul M

Full source

@[to_additive]
theorem Topology.IsInducing.continuousMul {M N F : Type*} [Mul M] [Mul N] [FunLike F M N]
    [MulHomClass F M N] [TopologicalSpace M] [TopologicalSpace N] [ContinuousMul N] (f : F)
    (hf : IsInducing f) : ContinuousMul M :=
  ⟨(hf.continuousSMul hf.continuous (map_mul f _ _)).1⟩

Induced Continuous Multiplication via Multiplicative Homomorphism

Informal description

Let $M$ and $N$ be types equipped with multiplication operations and topological structures, and let $F$ be a type of functions from $M$ to $N$ that preserves multiplication. Suppose $N$ has continuous multiplication, and $f \colon M \to N$ is a multiplicative homomorphism that induces the topology on $M$ (i.e., the topology on $M$ is the coinduced topology from $N$ via $f$). Then $M$ also has continuous multiplication.

continuousMul_induced theorem

 {M N F : Type*} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [TopologicalSpace N] [ContinuousMul N] (f : F) :
  @ContinuousMul M (induced f ‹_›) _

Full source

@[to_additive]
theorem continuousMul_induced {M N F : Type*} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N]
    [TopologicalSpace N] [ContinuousMul N] (f : F) : @ContinuousMul M (induced f ‹_›) _ :=
  letI := induced f ‹_›
  IsInducing.continuousMul f ⟨rfl⟩

Continuous Multiplication under Induced Topology via Multiplicative Homomorphism

Informal description

Let $M$ and $N$ be types equipped with multiplication operations, and let $F$ be a type of functions from $M$ to $N$ that preserves multiplication. Suppose $N$ is equipped with a topological space structure and has continuous multiplication. Then for any multiplicative homomorphism $f \colon M \to N$, the induced topology on $M$ (where open sets are preimages of open sets in $N$ under $f$) also makes the multiplication on $M$ continuous.

Subsemigroup.continuousMul instance

[TopologicalSpace M] [Semigroup M] [ContinuousMul M] (S : Subsemigroup M) : ContinuousMul S

Full source

@[to_additive]
instance Subsemigroup.continuousMul [TopologicalSpace M] [Semigroup M] [ContinuousMul M]
    (S : Subsemigroup M) : ContinuousMul S :=
  IsInducing.continuousMul ({ toFun := (↑), map_mul' := fun _ _ => rfl} : MulHom S M) ⟨rfl⟩

Continuous Multiplication in Subsemigroups

Informal description

For any topological semigroup $M$ with continuous multiplication and any subsemigroup $S$ of $M$, the multiplication operation on $S$ is also continuous with respect to the subspace topology.

Submonoid.continuousMul instance

[TopologicalSpace M] [Monoid M] [ContinuousMul M] (S : Submonoid M) : ContinuousMul S

Full source

@[to_additive]
instance Submonoid.continuousMul [TopologicalSpace M] [Monoid M] [ContinuousMul M]
    (S : Submonoid M) : ContinuousMul S :=
  S.toSubsemigroup.continuousMul

Continuous Multiplication in Submonoids

Informal description

For any topological monoid $M$ with continuous multiplication and any submonoid $S$ of $M$, the multiplication operation on $S$ is also continuous with respect to the subspace topology.

exists_mem_nhds_zero_mul_subset theorem

{K U : Set M} (hK : IsCompact K) (hU : U ∈ 𝓝 0) : ∃ V ∈ 𝓝 0, K * V ⊆ U

Full source

theorem exists_mem_nhds_zero_mul_subset
    {K U : Set M} (hK : IsCompact K) (hU : U ∈ 𝓝 0) : ∃ V ∈ 𝓝 0, K * V ⊆ U := by
  refine hK.induction_on ?_ ?_ ?_ ?_
  · exact ⟨univ, by simp⟩
  · rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
  · rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')
  · intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 0) by simpa using hU)
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

Existence of Neighborhood for Compact Multiplication in Topological Monoids

Informal description

For any compact set $K$ in a topological monoid $M$ and any neighborhood $U$ of the identity element $0$, there exists a neighborhood $V$ of $0$ such that the product set $K \cdot V$ is contained in $U$.

tendsto_mul_nhds_zero_prod_of_disjoint_cocompact theorem

{l : Filter M} (hl : Disjoint l (cocompact M)) : Tendsto (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l) (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map
`M × M → M` tends to zero on the filter product `𝓝 0 ×ˢ l`. -/
theorem tendsto_mul_nhds_zero_prod_of_disjoint_cocompact {l : Filter M}
    (hl : Disjoint l (cocompact M)) :
    Tendsto (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l) (𝓝 0) := calc
  mapmap (fun x : M × M ↦ x.1 * x.2) (𝓝 0 ×ˢ l)
  _ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ ({0} ×ˢ Set.univ)) :=
    map_mono <| nhds_prod_le_of_disjoint_cocompact 0 hl
  _ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨hx, _⟩ ↦ mul_eq_zero_of_left hx _

Convergence of Multiplication to Zero in Neighborhood-Cocompact Product Filter

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. For any filter $l$ on $M$ that is disjoint from the cocompact filter, the multiplication map $M \times M \to M$ given by $(x,y) \mapsto x \cdot y$ tends to $0$ on the filter product $\mathcal{N}_0 \times l$, where $\mathcal{N}_0$ is the neighborhood filter at $0$.

tendsto_mul_prod_nhds_zero_of_disjoint_cocompact theorem

{l : Filter M} (hl : Disjoint l (cocompact M)) : Tendsto (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0) (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M` which is disjoint from the cocompact filter. Then, the multiplication map
`M × M → M` tends to zero on the filter product `l ×ˢ 𝓝 0`. -/
theorem tendsto_mul_prod_nhds_zero_of_disjoint_cocompact {l : Filter M}
    (hl : Disjoint l (cocompact M)) :
    Tendsto (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0) (𝓝 0) := calc
  mapmap (fun x : M × M ↦ x.1 * x.2) (l ×ˢ 𝓝 0)
  _ ≤ map (fun x : M × M ↦ x.1 * x.2) (𝓝ˢ (Set.univ ×ˢ {0})) :=
    map_mono <| prod_nhds_le_of_disjoint_cocompact 0 hl
  _ ≤ 𝓝 0 := continuous_mul.tendsto_nhdsSet_nhds fun _ ⟨_, hx⟩ ↦ mul_eq_zero_of_right _ hx

Convergence of Multiplication to Zero under Disjoint Cocompact Filter

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. For any filter $l$ on $M$ that is disjoint from the cocompact filter, the multiplication map $M \times M \to M$ tends to $0$ on the filter product $l \times \mathcal{N}_0$, where $\mathcal{N}_0$ is the neighborhood filter at $0$.

tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact theorem

 {l : Filter (M × M)} (hl : Disjoint l (cocompact (M × M))) :
  Tendsto (fun x : M × M ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M × M` which is disjoint from the cocompact filter. Then, the multiplication
map `M × M → M` tends to zero on `(𝓝 0).coprod (𝓝 0) ⊓ l`. -/
theorem tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact {l : Filter (M × M)}
    (hl : Disjoint l (cocompact (M × M))) :
    Tendsto (fun x : M × M ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0) := by
  have := calc
    (𝓝 0).coprod (𝓝 0) ⊓ l
    _ ≤ (𝓝 0).coprod (𝓝 0) ⊓ map Prod.fst l ×ˢ map Prod.snd l :=
      inf_le_inf_left _ le_prod_map_fst_snd
    _ ≤ 𝓝𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0 :=
      coprod_inf_prod_le _ _ _ _
  apply (Tendsto.sup _ _).mono_left this
  · apply tendsto_mul_nhds_zero_prod_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_snd hl
  · apply tendsto_mul_prod_nhds_zero_of_disjoint_cocompact
    exact disjoint_map_cocompact continuous_fst hl

Convergence of Multiplication to Zero in Cocompact-Disjoint Filter Product

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. For any filter $l$ on $M \times M$ that is disjoint from the cocompact filter, the multiplication map $(x, y) \mapsto x \cdot y$ tends to $0$ on the filter $(\mathcal{N}_0 \times \mathcal{N}_0) \sqcap l$, where $\mathcal{N}_0$ is the neighborhood filter at $0$.

tendsto_mul_nhds_zero_of_disjoint_cocompact theorem

 {l : Filter (M × M)} (hl : Disjoint l (cocompact (M × M))) (h'l : l ≤ (𝓝 0).coprod (𝓝 0)) :
  Tendsto (fun x : M × M ↦ x.1 * x.2) l (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M × M` which is both disjoint from the cocompact filter and less than or
equal to `(𝓝 0).coprod (𝓝 0)`. Then the multiplication map `M × M → M` tends to zero on `l`. -/
theorem tendsto_mul_nhds_zero_of_disjoint_cocompact {l : Filter (M × M)}
    (hl : Disjoint l (cocompact (M × M))) (h'l : l ≤ (𝓝 0).coprod (𝓝 0)) :
    Tendsto (fun x : M × M ↦ x.1 * x.2) l (𝓝 0) := by
  simpa [inf_eq_right.mpr h'l] using tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact hl

Convergence of Multiplication to Zero under Cocompact-Disjoint and Neighborhood Conditions

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. For any filter $l$ on $M \times M$ that is disjoint from the cocompact filter and satisfies $l \leq \mathcal{N}_0 \times \mathcal{N}_0$, the multiplication map $(x, y) \mapsto x \cdot y$ tends to $0$ along $l$, where $\mathcal{N}_0$ is the neighborhood filter at $0$.

Tendsto.tendsto_mul_zero_of_disjoint_cocompact_right theorem

 {f g : α → M} {l : Filter α} (hf : Tendsto f l (𝓝 0)) (hg : Disjoint (map g l) (cocompact M)) :
  Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `f : α → M` and `g : α → M` be functions. If `f` tends to zero on a filter `l`
and the image of `l` under `g` is disjoint from the cocompact filter on `M`, then
`fun x : α ↦ f x * g x` also tends to zero on `l`. -/
theorem Tendsto.tendsto_mul_zero_of_disjoint_cocompact_right {f g : α → M} {l : Filter α}
    (hf : Tendsto f l (𝓝 0)) (hg : Disjoint (map g l) (cocompact M)) :
    Tendsto (fun x ↦ f x * g x) l (𝓝 0) :=
  tendsto_mul_nhds_zero_prod_of_disjoint_cocompact hg |>.comp (hf.prodMk tendsto_map)

Product of Zero-Tending and Cocompact-Disjoint Functions Tends to Zero

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. Let $f, g : \alpha \to M$ be functions and $l$ a filter on $\alpha$. If $f$ tends to $0$ along $l$ and the image of $l$ under $g$ is disjoint from the cocompact filter on $M$, then the function $x \mapsto f(x) \cdot g(x)$ tends to $0$ along $l$.

Tendsto.tendsto_mul_zero_of_disjoint_cocompact_left theorem

 {f g : α → M} {l : Filter α} (hf : Disjoint (map f l) (cocompact M)) (hg : Tendsto g l (𝓝 0)) :
  Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Full source

/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `f : α → M` and `g : α → M` be functions. If `g` tends to zero on a filter `l`
and the image of `l` under `f` is disjoint from the cocompact filter on `M`, then
`fun x : α ↦ f x * g x` also tends to zero on `l`. -/
theorem Tendsto.tendsto_mul_zero_of_disjoint_cocompact_left {f g : α → M} {l : Filter α}
    (hf : Disjoint (map f l) (cocompact M)) (hg : Tendsto g l (𝓝 0)):
    Tendsto (fun x ↦ f x * g x) l (𝓝 0) :=
  tendsto_mul_prod_nhds_zero_of_disjoint_cocompact hf |>.comp (tendsto_map.prodMk hg)

Convergence of Product to Zero under Disjoint Cocompact Condition (Left Version)

Informal description

Let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. Let $f, g : \alpha \to M$ be functions and $l$ a filter on $\alpha$. If the image of $l$ under $f$ is disjoint from the cocompact filter on $M$ and $g$ tends to $0$ along $l$, then the function $x \mapsto f(x) * g(x)$ also tends to $0$ along $l$.

tendsto_mul_cocompact_nhds_zero theorem

 [TopologicalSpace α] [TopologicalSpace β] {f : α → M} {g : β → M} (f_cont : Continuous f) (g_cont : Continuous g)
  (hf : Tendsto f (cocompact α) (𝓝 0)) (hg : Tendsto g (cocompact β) (𝓝 0)) :
  Tendsto (fun i : α × β ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0)

Full source

/-- If `f : α → M` and `g : β → M` are continuous and both tend to zero on the cocompact filter,
then `fun i : α × β ↦ f i.1 * g i.2` also tends to zero on the cocompact filter. -/
theorem tendsto_mul_cocompact_nhds_zero [TopologicalSpace α] [TopologicalSpace β]
    {f : α → M} {g : β → M} (f_cont : Continuous f) (g_cont : Continuous g)
    (hf : Tendsto f (cocompact α) (𝓝 0)) (hg : Tendsto g (cocompact β) (𝓝 0)) :
    Tendsto (fun i : α × β ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0) := by
  set l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β)) with l_def
  set K : Set (M × M) := (insert 0 (range f)) ×ˢ (insert 0 (range g))
  have K_compact : IsCompact K := .prod (hf.isCompact_insert_range_of_cocompact f_cont)
    (hg.isCompact_insert_range_of_cocompact g_cont)
  have K_mem_l : K ∈ l := eventually_map.mpr <| .of_forall fun ⟨x, y⟩ ↦
    ⟨mem_insert_of_mem _ (mem_range_self _), mem_insert_of_mem _ (mem_range_self _)⟩
  have l_compact : Disjoint l (cocompact (M × M)) := by
    rw [disjoint_cocompact_right]
    exact ⟨K, K_mem_l, K_compact⟩
  have l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0) := by
    rw [l_def, ← coprod_cocompact]
    exact hf.prodMap_coprod hg
  exact tendsto_mul_nhds_zero_of_disjoint_cocompact l_compact l_le_coprod |>.comp tendsto_map

Product of Cocompactly Vanishing Continuous Functions Tends to Zero

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $M$ be a topological space with a continuous multiplication operation and an identity element $0$. Given continuous functions $f \colon \alpha \to M$ and $g \colon \beta \to M$ such that $f$ tends to $0$ along the cocompact filter of $\alpha$ and $g$ tends to $0$ along the cocompact filter of $\beta$, the function $(x, y) \mapsto f(x) \cdot g(y)$ tends to $0$ along the cocompact filter of $\alpha \times \beta$.

tendsto_mul_cofinite_nhds_zero theorem

 {f : α → M} {g : β → M} (hf : Tendsto f cofinite (𝓝 0)) (hg : Tendsto g cofinite (𝓝 0)) :
  Tendsto (fun i : α × β ↦ f i.1 * g i.2) cofinite (𝓝 0)

Full source

/-- If `f : α → M` and `g : β → M` both tend to zero on the cofinite filter, then so does
`fun i : α × β ↦ f i.1 * g i.2`. -/
theorem tendsto_mul_cofinite_nhds_zero {f : α → M} {g : β → M}
    (hf : Tendsto f cofinite (𝓝 0)) (hg : Tendsto g cofinite (𝓝 0)) :
    Tendsto (fun i : α × β ↦ f i.1 * g i.2) cofinite (𝓝 0) := by
  letI : TopologicalSpace α := ⊥
  haveI : DiscreteTopology α := discreteTopology_bot α
  letI : TopologicalSpace β := ⊥
  haveI : DiscreteTopology β := discreteTopology_bot β
  rw [← cocompact_eq_cofinite] at *
  exact tendsto_mul_cocompact_nhds_zero
    continuous_of_discreteTopology continuous_of_discreteTopology hf hg

Product of Cofinitely Vanishing Functions Tends to Zero

Informal description

Let $f \colon \alpha \to M$ and $g \colon \beta \to M$ be functions such that $f$ tends to $0$ along the cofinite filter on $\alpha$ and $g$ tends to $0$ along the cofinite filter on $\beta$. Then the function $(x, y) \mapsto f(x) \cdot g(y)$ tends to $0$ along the cofinite filter on $\alpha \times \beta$.

GroupWithZero.isOpen_singleton_zero theorem

[GroupWithZero M] [TopologicalSpace M] [ContinuousMul M] [CompactSpace M] [T1Space M] : IsOpen {(0 : M)}

Full source

lemma GroupWithZero.isOpen_singleton_zero [GroupWithZero M] [TopologicalSpace M]
    [ContinuousMul M] [CompactSpace M] [T1Space M] :
    IsOpen {(0 : M)} := by
  obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one
  obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)
  by_cases H : ∃ x ≠ 0, x ∈ W
  · obtain ⟨x, hx, hxW⟩ := H
    cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))
  · obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
    simpa [isOpen_iff_mem_nhds]

Openness of Zero in Compact $T_1$ Topological Group with Zero

Informal description

Let $M$ be a topological group with zero, equipped with a continuous multiplication operation. If $M$ is a compact space and satisfies the $T_1$ separation axiom, then the singleton set $\{0\}$ is open in $M$.

exists_open_nhds_one_split theorem

 {s : Set M} (hs : s ∈ 𝓝 (1 : M)) : ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Full source

@[to_additive exists_open_nhds_zero_half]
theorem exists_open_nhds_one_split {s : Set M} (hs : s ∈ 𝓝 (1 : M)) :
    ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s := by
  have : (fun a : M × M => a.1 * a.2) ⁻¹' s(fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) :=
    tendsto_mul (by simpa only [one_mul] using hs)
  simpa only [prod_subset_iff] using exists_nhds_square this

Existence of Open Neighborhood of Identity with Multiplicative Closure Property

Informal description

For any neighborhood $s$ of the identity element $1$ in a topological monoid $M$, there exists an open neighborhood $V$ of $1$ such that for any $v, w \in V$, the product $v * w$ belongs to $s$.

exists_nhds_one_split theorem

{s : Set M} (hs : s ∈ 𝓝 (1 : M)) : ∃ V ∈ 𝓝 (1 : M), ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s

Full source

@[to_additive exists_nhds_zero_half]
theorem exists_nhds_one_split {s : Set M} (hs : s ∈ 𝓝 (1 : M)) :
    ∃ V ∈ 𝓝 (1 : M), ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s :=
  let ⟨V, Vo, V1, hV⟩ := exists_open_nhds_one_split hs
  ⟨V, IsOpen.mem_nhds Vo V1, hV⟩

Existence of Multiplicatively Closed Neighborhood of Identity in Topological Monoid

Informal description

For any neighborhood $s$ of the identity element $1$ in a topological monoid $M$, there exists a neighborhood $V$ of $1$ such that for any $v, w \in V$, the product $v \cdot w$ belongs to $s$.

exists_open_nhds_one_mul_subset theorem

{U : Set M} (hU : U ∈ 𝓝 (1 : M)) : ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ V * V ⊆ U

Full source

/-- Given a neighborhood `U` of `1` there is an open neighborhood `V` of `1`
such that `V * V ⊆ U`. -/
@[to_additive "Given an open neighborhood `U` of `0` there is an open neighborhood `V` of `0`
  such that `V + V ⊆ U`."]
theorem exists_open_nhds_one_mul_subset {U : Set M} (hU : U ∈ 𝓝 (1 : M)) :
    ∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ V * V ⊆ U := by
  simpa only [mul_subset_iff] using exists_open_nhds_one_split hU

Existence of Open Neighborhood with Square Contained in Given Neighborhood

Informal description

For any neighborhood $U$ of the identity element $1$ in a topological monoid $M$, there exists an open neighborhood $V$ of $1$ such that the product set $V \cdot V$ is contained in $U$.

Filter.HasBasis.mul_self theorem

{p : ι → Prop} {s : ι → Set M} (h : (𝓝 1).HasBasis p s) : (𝓝 1).HasBasis p fun i => s i * s i

Full source

@[to_additive]
theorem Filter.HasBasis.mul_self {p : ι → Prop} {s : ι → Set M} (h : (𝓝 1).HasBasis p s) :
    (𝓝 1).HasBasis p fun i => s i * s i := by
  rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]
  simpa only [← image_mul_prod] using h.prod_self.map _

Neighborhood Basis of Identity via Square Sets in Topological Monoid

Informal description

Let $M$ be a topological monoid with identity element $1$, and suppose the neighborhood filter $\mathcal{N}_1$ has a basis $\{s_i\}_{i \in \iota}$ indexed by a predicate $p$. Then the neighborhood filter $\mathcal{N}_1$ also has a basis given by $\{s_i \cdot s_i\}_{i \in \iota}$ with the same index predicate $p$.

Subsemigroup.top_closure_mul_self_subset theorem

(s : Subsemigroup M) : _root_.closure (s : Set M) * _root_.closure s ⊆ _root_.closure s

Full source

@[to_additive]
theorem Subsemigroup.top_closure_mul_self_subset (s : Subsemigroup M) :
    _root_.closure_root_.closure (s : Set M) * _root_.closure s ⊆ _root_.closure s :=
  image2_subset_iff.2 fun _ hx _ hy =>
    map_mem_closure₂ continuous_mul hx hy fun _ ha _ hb => s.mul_mem ha hb

Closure of Subsemigroup is Closed Under Multiplication

Informal description

For any subsemigroup $s$ of a topological monoid $M$, the product of the topological closure of $s$ with itself is contained in the topological closure of $s$. In other words, if $x, y \in \overline{s}$, then $x \cdot y \in \overline{s}$.

Subsemigroup.topologicalClosure definition

(s : Subsemigroup M) : Subsemigroup M

Full source

/-- The (topological-space) closure of a subsemigroup of a space `M` with `ContinuousMul` is
itself a subsemigroup. -/
@[to_additive "The (topological-space) closure of an additive submonoid of a space `M` with
`ContinuousAdd` is itself an additive submonoid."]
def Subsemigroup.topologicalClosure (s : Subsemigroup M) : Subsemigroup M where
  carrier := _root_.closure (s : Set M)
  mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩

Topological closure of a subsemigroup

Informal description

Given a subsemigroup $s$ of a topological space $M$ with continuous multiplication, the topological closure of $s$ is itself a subsemigroup. Specifically, the underlying set of the closure is the topological closure of the underlying set of $s$, and it is closed under multiplication.

Subsemigroup.coe_topologicalClosure theorem

(s : Subsemigroup M) : (s.topologicalClosure : Set M) = _root_.closure (s : Set M)

Full source

@[to_additive]
theorem Subsemigroup.coe_topologicalClosure (s : Subsemigroup M) :
    (s.topologicalClosure : Set M) = _root_.closure (s : Set M) := rfl

Equality of Subsemigroup Closure and Set Closure

Informal description

For any subsemigroup $s$ of a topological space $M$ with continuous multiplication, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$, i.e., $\overline{s} = \overline{(s : \text{Set } M)}$.

Subsemigroup.le_topologicalClosure theorem

(s : Subsemigroup M) : s ≤ s.topologicalClosure

Full source

@[to_additive]
theorem Subsemigroup.le_topologicalClosure (s : Subsemigroup M) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subsemigroup is Contained in its Topological Closure

Informal description

For any subsemigroup $s$ of a topological space $M$ with continuous multiplication, $s$ is contained in its topological closure, i.e., $s \subseteq \overline{s}$.

Subsemigroup.isClosed_topologicalClosure theorem

(s : Subsemigroup M) : IsClosed (s.topologicalClosure : Set M)

Full source

@[to_additive]
theorem Subsemigroup.isClosed_topologicalClosure (s : Subsemigroup M) :
    IsClosed (s.topologicalClosure : Set M) := isClosed_closure

Topological Closure of a Subsemigroup is Closed

Informal description

For any subsemigroup $s$ of a topological space $M$ with continuous multiplication, the topological closure of $s$ is a closed set in $M$.

Subsemigroup.topologicalClosure_minimal theorem

(s : Subsemigroup M) {t : Subsemigroup M} (h : s ≤ t) (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t

Full source

@[to_additive]
theorem Subsemigroup.topologicalClosure_minimal (s : Subsemigroup M) {t : Subsemigroup M}
    (h : s ≤ t) (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t := closure_minimal h ht

Minimality of Topological Closure for Subsemigroups

Informal description

Let $s$ and $t$ be subsemigroups of a topological monoid $M$ with continuous multiplication. If $s$ is contained in $t$ and $t$ is closed, then the topological closure of $s$ is also contained in $t$.

Subsemigroup.commSemigroupTopologicalClosure abbrev

[T2Space M] (s : Subsemigroup M) (hs : ∀ x y : s, x * y = y * x) : CommSemigroup s.topologicalClosure

Full source

/-- If a subsemigroup of a topological semigroup is commutative, then so is its topological
closure.

See note [reducible non-instances] -/
@[to_additive "If a submonoid of an additive topological monoid is commutative, then so is its
topological closure.

See note [reducible non-instances]"]
abbrev Subsemigroup.commSemigroupTopologicalClosure [T2Space M] (s : Subsemigroup M)
    (hs : ∀ x y : s, x * y = y * x) : CommSemigroup s.topologicalClosure :=
  { MulMemClass.toSemigroup s.topologicalClosure with
    mul_comm :=
      have : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x := fun x hx y hy =>
        congr_arg Subtype.val (hs ⟨x, hx⟩ ⟨y, hy⟩)
      fun ⟨x, hx⟩ ⟨y, hy⟩ =>
      Subtype.ext <|
        eqOn_closure₂ this continuous_mul (continuous_snd.mul continuous_fst) x hx y hy }

Commutativity of Topological Closure for Commutative Subsemigroups

Informal description

Let $M$ be a Hausdorff topological space with continuous multiplication. If $s$ is a subsemigroup of $M$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$, then the topological closure of $s$ is a commutative semigroup.

IsCompact.mul theorem

{s t : Set M} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s * t)

Full source

@[to_additive]
theorem IsCompact.mul {s t : Set M} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s * t) := by
  rw [← image_mul_prod]
  exact (hs.prod ht).image continuous_mul

Product of Compact Sets is Compact in Topological Monoid

Informal description

For any two compact subsets $s$ and $t$ of a topological monoid $M$, the product set $s \cdot t$ is compact.

Submonoid.top_closure_mul_self_subset theorem

(s : Submonoid M) : _root_.closure (s : Set M) * _root_.closure s ⊆ _root_.closure s

Full source

@[to_additive]
theorem Submonoid.top_closure_mul_self_subset (s : Submonoid M) :
    _root_.closure_root_.closure (s : Set M) * _root_.closure s ⊆ _root_.closure s :=
  image2_subset_iff.2 fun _ hx _ hy =>
    map_mem_closure₂ continuous_mul hx hy fun _ ha _ hb => s.mul_mem ha hb

Closure of Submonoid is Closed Under Multiplication

Informal description

For any submonoid $s$ of a topological monoid $M$, the product of the topological closure of $s$ with itself is contained in the topological closure of $s$, i.e., $\overline{s} \cdot \overline{s} \subseteq \overline{s}$.

Submonoid.top_closure_mul_self_eq theorem

(s : Submonoid M) : _root_.closure (s : Set M) * _root_.closure s = _root_.closure s

Full source

@[to_additive]
theorem Submonoid.top_closure_mul_self_eq (s : Submonoid M) :
    _root_.closure (s : Set M) * _root_.closure s = _root_.closure s :=
  Subset.antisymm s.top_closure_mul_self_subset fun x hx =>
    ⟨x, hx, 1, _root_.subset_closure s.one_mem, mul_one _⟩

Closure of Submonoid is Closed Under Multiplication and Equals Its Own Product

Informal description

For any submonoid $s$ of a topological monoid $M$ with continuous multiplication, the product of the topological closure of $s$ with itself equals the topological closure of $s$, i.e., $\overline{s} \cdot \overline{s} = \overline{s}$.

Submonoid.topologicalClosure definition

(s : Submonoid M) : Submonoid M

Full source

/-- The (topological-space) closure of a submonoid of a space `M` with `ContinuousMul` is
itself a submonoid. -/
@[to_additive "The (topological-space) closure of an additive submonoid of a space `M` with
`ContinuousAdd` is itself an additive submonoid."]
def Submonoid.topologicalClosure (s : Submonoid M) : Submonoid M where
  carrier := _root_.closure (s : Set M)
  one_mem' := _root_.subset_closure s.one_mem
  mul_mem' ha hb := s.top_closure_mul_self_subset ⟨_, ha, _, hb, rfl⟩

Topological closure of a submonoid

Informal description

Given a submonoid $ s $ of a topological monoid $ M $ with continuous multiplication, the topological closure of $ s $ is itself a submonoid of $ M $. The underlying set of this closure is the topological closure of the underlying set of $ s $, and it contains the identity element and is closed under multiplication.

Submonoid.coe_topologicalClosure theorem

(s : Submonoid M) : (s.topologicalClosure : Set M) = _root_.closure (s : Set M)

Full source

@[to_additive]
theorem Submonoid.coe_topologicalClosure (s : Submonoid M) :
    (s.topologicalClosure : Set M) = _root_.closure (s : Set M) := rfl

Equality of Submonoid Closure and Set Closure in Topological Monoids

Informal description

For any submonoid $s$ of a topological monoid $M$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$, i.e., $\overline{s} = \overline{(s : \text{Set } M)}$.

Submonoid.le_topologicalClosure theorem

(s : Submonoid M) : s ≤ s.topologicalClosure

Full source

@[to_additive]
theorem Submonoid.le_topologicalClosure (s : Submonoid M) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Submonoid is Contained in its Topological Closure

Informal description

For any submonoid $s$ of a topological monoid $M$ with continuous multiplication, the submonoid $s$ is contained in its topological closure, i.e., $s \leq \overline{s}$.

Submonoid.isClosed_topologicalClosure theorem

(s : Submonoid M) : IsClosed (s.topologicalClosure : Set M)

Full source

@[to_additive]
theorem Submonoid.isClosed_topologicalClosure (s : Submonoid M) :
    IsClosed (s.topologicalClosure : Set M) := isClosed_closure

Topological Closure of Submonoid is Closed

Informal description

For any submonoid $s$ of a topological monoid $M$, the topological closure of $s$ is a closed subset of $M$.

Submonoid.topologicalClosure_minimal theorem

(s : Submonoid M) {t : Submonoid M} (h : s ≤ t) (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t

Full source

@[to_additive]
theorem Submonoid.topologicalClosure_minimal (s : Submonoid M) {t : Submonoid M} (h : s ≤ t)
    (ht : IsClosed (t : Set M)) : s.topologicalClosure ≤ t := closure_minimal h ht

Minimality of Topological Closure for Submonoids

Informal description

Let $ s $ and $ t $ be submonoids of a topological monoid $ M $ with continuous multiplication. If $ s $ is contained in $ t $ and the underlying set of $ t $ is closed, then the topological closure of $ s $ is also contained in $ t $.

Submonoid.commMonoidTopologicalClosure abbrev

[T2Space M] (s : Submonoid M) (hs : ∀ x y : s, x * y = y * x) : CommMonoid s.topologicalClosure

Full source

/-- If a submonoid of a topological monoid is commutative, then so is its topological closure. -/
@[to_additive "If a submonoid of an additive topological monoid is commutative, then so is its
topological closure.

See note [reducible non-instances]."]
abbrev Submonoid.commMonoidTopologicalClosure [T2Space M] (s : Submonoid M)
    (hs : ∀ x y : s, x * y = y * x) : CommMonoid s.topologicalClosure :=
  { s.topologicalClosure.toMonoid, s.toSubsemigroup.commSemigroupTopologicalClosure hs with }

Commutativity of Topological Closure for Commutative Submonoids

Informal description

Let $M$ be a Hausdorff topological monoid with continuous multiplication. If $s$ is a submonoid of $M$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$, then the topological closure of $s$ is a commutative monoid.

exists_nhds_one_split4 theorem

 {u : Set M} (hu : u ∈ 𝓝 (1 : M)) : ∃ V ∈ 𝓝 (1 : M), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Full source

@[to_additive exists_nhds_zero_quarter]
theorem exists_nhds_one_split4 {u : Set M} (hu : u ∈ 𝓝 (1 : M)) :
    ∃ V ∈ 𝓝 (1 : M), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u := by
  rcases exists_nhds_one_split hu with ⟨W, W1, h⟩
  rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩
  use V, V1
  intro v w s t v_in w_in s_in t_in
  simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)

Existence of Quadruple-Product-Closed Neighborhood of Identity in Topological Monoid

Informal description

For any neighborhood $u$ of the identity element $1$ in a topological monoid $M$, there exists a neighborhood $V$ of $1$ such that for any four elements $v, w, s, t \in V$, the product $v \cdot w \cdot s \cdot t$ belongs to $u$.

tendsto_list_prod theorem

 {f : ι → α → M} {x : Filter α} {a : ι → M} :
  ∀ l : List ι,
    (∀ i ∈ l, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => (l.map fun c => f c b).prod) x (𝓝 (l.map a).prod)

Full source

@[to_additive]
theorem tendsto_list_prod {f : ι → α → M} {x : Filter α} {a : ι → M} :
    ∀ l : List ι,
      (∀ i ∈ l, Tendsto (f i) x (𝓝 (a i))) →
        Tendsto (fun b => (l.map fun c => f c b).prod) x (𝓝 (l.map a).prod)
  | [], _ => by simp [tendsto_const_nhds]
  | f::l, h => by
    simp only [List.map_cons, List.prod_cons]
    exact
      (h f List.mem_cons_self).mul
        (tendsto_list_prod l fun c hc => h c (List.mem_cons_of_mem _ hc))

Limit of Product of Functions in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $\{f_i : \alpha \to M\}_{i \in \iota}$ a family of functions, $x$ a filter on $\alpha$, and $\{a_i\}_{i \in \iota}$ a family of points in $M$. For any list $l$ of indices in $\iota$, if for each $i \in l$ the function $f_i$ tends to $a_i$ along the filter $x$, then the product $\prod_{i \in l} f_i(b)$ tends to $\prod_{i \in l} a_i$ along $x$ as $b$ varies.

continuous_list_prod theorem

 {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) : Continuous fun a => (l.map fun i => f i a).prod

Full source

@[to_additive (attr := continuity)]
theorem continuous_list_prod {f : ι → X → M} (l : List ι) (h : ∀ i ∈ l, Continuous (f i)) :
    Continuous fun a => (l.map fun i => f i a).prod :=
  continuous_iff_continuousAt.2 fun x =>
    tendsto_list_prod l fun c hc => continuous_iff_continuousAt.1 (h c hc) x

Continuity of Finite Products of Continuous Functions in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $X$ a topological space, and $\{f_i : X \to M\}_{i \in \iota}$ a family of continuous functions. For any list $l$ of indices in $\iota$, if each function $f_i$ with $i \in l$ is continuous, then the product function $a \mapsto \prod_{i \in l} f_i(a)$ is continuous on $X$.

continuousOn_list_prod theorem

 {f : ι → X → M} (l : List ι) {t : Set X} (h : ∀ i ∈ l, ContinuousOn (f i) t) :
  ContinuousOn (fun a => (l.map fun i => f i a).prod) t

Full source

@[to_additive]
theorem continuousOn_list_prod {f : ι → X → M} (l : List ι) {t : Set X}
    (h : ∀ i ∈ l, ContinuousOn (f i) t) :
    ContinuousOn (fun a => (l.map fun i => f i a).prod) t := by
  intro x hx
  rw [continuousWithinAt_iff_continuousAt_restrict _ hx]
  refine tendsto_list_prod _ fun i hi => ?_
  specialize h i hi x hx
  rw [continuousWithinAt_iff_continuousAt_restrict _ hx] at h
  exact h

Continuity of Product of Functions on a Subset in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $\{f_i : X \to M\}_{i \in \iota}$ a family of functions, and $t \subseteq X$. For any list $l$ of indices in $\iota$, if each function $f_i$ for $i \in l$ is continuous on $t$, then the product function $\prod_{i \in l} f_i$ is continuous on $t$.

continuous_pow theorem

: ∀ n : ℕ, Continuous fun a : M => a ^ n

Full source

@[to_additive (attr := continuity)]
theorem continuous_pow : ∀ n : ℕ, Continuous fun a : M => a ^ n
  | 0 => by simpa using continuous_const
  | k + 1 => by
    simp only [pow_succ']
    exact continuous_id.mul (continuous_pow _)

Continuity of the power function on a topological monoid

Informal description

For any natural number $n$, the function $a \mapsto a^n$ is continuous on a topological monoid $M$.

AddMonoid.continuousConstSMul_nat instance

{A} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousConstSMul ℕ A

Full source

instance AddMonoid.continuousConstSMul_nat {A} [AddMonoid A] [TopologicalSpace A]
    [ContinuousAdd A] : ContinuousConstSMul ℕ A :=
  ⟨continuous_nsmul⟩

Continuous Scalar Multiplication by Natural Numbers on Additive Monoids

Informal description

For any additive monoid $A$ with a topological space structure and continuous addition, the scalar multiplication by natural numbers is continuous in the second variable.

AddMonoid.continuousSMul_nat instance

{A} [AddMonoid A] [TopologicalSpace A] [ContinuousAdd A] : ContinuousSMul ℕ A

Full source

instance AddMonoid.continuousSMul_nat {A} [AddMonoid A] [TopologicalSpace A]
    [ContinuousAdd A] : ContinuousSMul ℕ A :=
  ⟨continuous_prod_of_discrete_left.mpr continuous_nsmul⟩

Joint Continuity of Natural Scalar Multiplication on Topological Additive Monoids

Informal description

For any additive monoid $A$ with a topological space structure and continuous addition, the scalar multiplication operation $\mathbb{N} \times A \to A$ is jointly continuous.

Continuous.pow theorem

{f : X → M} (h : Continuous f) (n : ℕ) : Continuous fun b => f b ^ n

Full source

@[to_additive (attr := aesop safe -100 (rule_sets := [Continuous]), fun_prop)]
theorem Continuous.pow {f : X → M} (h : Continuous f) (n : ℕ) : Continuous fun b => f b ^ n :=
  (continuous_pow n).comp h

Continuity of powers of continuous functions

Informal description

Let $f : X \to M$ be a continuous function from a topological space $X$ to a topological monoid $M$. Then for any natural number $n$, the function $x \mapsto (f(x))^n$ is continuous on $X$.

continuousOn_pow theorem

{s : Set M} (n : ℕ) : ContinuousOn (fun (x : M) => x ^ n) s

Full source

@[to_additive]
theorem continuousOn_pow {s : Set M} (n : ℕ) : ContinuousOn (fun (x : M) => x ^ n) s :=
  (continuous_pow n).continuousOn

Continuity of power function on subsets of a topological monoid

Informal description

For any subset $s$ of a topological monoid $M$ and any natural number $n$, the function $x \mapsto x^n$ is continuous on $s$.

continuousAt_pow theorem

(x : M) (n : ℕ) : ContinuousAt (fun (x : M) => x ^ n) x

Full source

@[to_additive]
theorem continuousAt_pow (x : M) (n : ℕ) : ContinuousAt (fun (x : M) => x ^ n) x :=
  (continuous_pow n).continuousAt

Continuity of the power function at a point in a topological monoid

Informal description

For any element $x$ in a topological monoid $M$ and any natural number $n$, the function $x \mapsto x^n$ is continuous at $x$.

Filter.Tendsto.pow theorem

 {l : Filter α} {f : α → M} {x : M} (hf : Tendsto f l (𝓝 x)) (n : ℕ) : Tendsto (fun x => f x ^ n) l (𝓝 (x ^ n))

Full source

@[to_additive]
theorem Filter.Tendsto.pow {l : Filter α} {f : α → M} {x : M} (hf : Tendsto f l (𝓝 x)) (n : ℕ) :
    Tendsto (fun x => f x ^ n) l (𝓝 (x ^ n)) :=
  (continuousAt_pow _ _).tendsto.comp hf

Limit of Powers in Topological Monoids

Informal description

Let $l$ be a filter on a type $\alpha$, $f : \alpha \to M$ a function to a topological monoid $M$, and $x \in M$. If $f$ tends to $x$ along $l$, then for any natural number $n$, the function $x \mapsto f(x)^n$ tends to $x^n$ along $l$.

ContinuousWithinAt.pow theorem

{f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x) (n : ℕ) : ContinuousWithinAt (fun x => f x ^ n) s x

Full source

@[to_additive]
theorem ContinuousWithinAt.pow {f : X → M} {x : X} {s : Set X} (hf : ContinuousWithinAt f s x)
    (n : ℕ) : ContinuousWithinAt (fun x => f x ^ n) s x :=
  Filter.Tendsto.pow hf n

Continuity of powers within a set at a point in topological monoids

Informal description

Let $X$ be a topological space, $M$ a topological monoid, $f : X \to M$ a function, $x \in X$, and $s \subseteq X$. If $f$ is continuous within $s$ at $x$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also continuous within $s$ at $x$.

ContinuousAt.pow theorem

{f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) : ContinuousAt (fun x => f x ^ n) x

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousAt.pow {f : X → M} {x : X} (hf : ContinuousAt f x) (n : ℕ) :
    ContinuousAt (fun x => f x ^ n) x :=
  Filter.Tendsto.pow hf n

Continuity of powers at a point in topological monoids

Informal description

Let $X$ be a topological space, $M$ a topological monoid, $f : X \to M$ a function, and $x \in X$. If $f$ is continuous at $x$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also continuous at $x$.

ContinuousOn.pow theorem

{f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) : ContinuousOn (fun x => f x ^ n) s

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousOn.pow {f : X → M} {s : Set X} (hf : ContinuousOn f s) (n : ℕ) :
    ContinuousOn (fun x => f x ^ n) s := fun x hx => (hf x hx).pow n

Continuity of powers on a set in topological monoids

Informal description

Let $X$ be a topological space, $M$ a topological monoid, $f : X \to M$ a function, and $s \subseteq X$. If $f$ is continuous on $s$, then for any natural number $n$, the function $x \mapsto f(x)^n$ is also continuous on $s$.

Filter.tendsto_cocompact_mul_left theorem

{a b : M} (ha : b * a = 1) : Filter.Tendsto (fun x : M => a * x) (Filter.cocompact M) (Filter.cocompact M)

Full source

/-- Left-multiplication by a left-invertible element of a topological monoid is proper, i.e.,
inverse images of compact sets are compact. -/
theorem Filter.tendsto_cocompact_mul_left {a b : M} (ha : b * a = 1) :
    Filter.Tendsto (fun x : M => a * x) (Filter.cocompact M) (Filter.cocompact M) := by
  refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_left b))
  convert Filter.tendsto_id
  ext x
  simp [← mul_assoc, ha]

Properness of Left Multiplication by a Left-Invertible Element in Topological Monoids

Informal description

Let $M$ be a topological monoid and let $a, b \in M$ such that $b * a = 1$. Then the left-multiplication map $x \mapsto a * x$ is proper, i.e., it maps cocompact sets to cocompact sets.

Filter.tendsto_cocompact_mul_right theorem

{a b : M} (ha : a * b = 1) : Filter.Tendsto (fun x : M => x * a) (Filter.cocompact M) (Filter.cocompact M)

Full source

/-- Right-multiplication by a right-invertible element of a topological monoid is proper, i.e.,
inverse images of compact sets are compact. -/
theorem Filter.tendsto_cocompact_mul_right {a b : M} (ha : a * b = 1) :
    Filter.Tendsto (fun x : M => x * a) (Filter.cocompact M) (Filter.cocompact M) := by
  refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))
  simp only [comp_mul_right, ha, mul_one]
  exact Filter.tendsto_id

Properness of right multiplication by a right-invertible element in a topological monoid

Informal description

Let $M$ be a topological monoid and let $a, b \in M$ be elements such that $a * b = 1$. Then the right multiplication map $x \mapsto x * a$ is proper, i.e., it maps cocompact sets to cocompact sets. In other words, the preimage of any compact set under this map is compact.

IsScalarTower.continuousConstSMul instance

 {R A : Type*} [Monoid A] [SMul R A] [IsScalarTower R A A] [TopologicalSpace A] [ContinuousMul A] :
  ContinuousConstSMul R A

Full source

/-- If `R` acts on `A` via `A`, then continuous multiplication implies continuous scalar
multiplication by constants.

Notably, this instances applies when `R = A`, or when `[Algebra R A]` is available. -/
@[to_additive "If `R` acts on `A` via `A`, then continuous addition implies
continuous affine addition by constants."]
instance (priority := 100) IsScalarTower.continuousConstSMul {R A : Type*} [Monoid A] [SMul R A]
    [IsScalarTower R A A] [TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul R A where
  continuous_const_smul q := by
    simp +singlePass only [← smul_one_mul q (_ : A)]
    exact continuous_const.mul continuous_id

Continuous Scalar Multiplication via Monoid Action

Informal description

Let $R$ and $A$ be types, where $A$ is a monoid with a scalar multiplication action by $R$ such that $R$ acts on $A$ via $A$ (i.e., $[IsScalarTower R A A]$). If $A$ is equipped with a topological space structure and has continuous multiplication, then the scalar multiplication by any fixed element of $R$ is continuous in $A$.

SMulCommClass.continuousConstSMul instance

 {R A : Type*} [Monoid A] [SMul R A] [SMulCommClass R A A] [TopologicalSpace A] [ContinuousMul A] :
  ContinuousConstSMul R A

Full source

/-- If the action of `R` on `A` commutes with left-multiplication, then continuous multiplication
implies continuous scalar multiplication by constants.

Notably, this instances applies when `R = Aᵐᵒᵖ`. -/
@[to_additive "If the action of `R` on `A` commutes with left-addition, then
continuous addition implies continuous affine addition by constants.

Notably, this instances applies when `R = Aᵃᵒᵖ`."]
instance (priority := 100) SMulCommClass.continuousConstSMul {R A : Type*} [Monoid A] [SMul R A]
    [SMulCommClass R A A] [TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul R A where
  continuous_const_smul q := by
    simp +singlePass only [← mul_smul_one q (_ : A)]
    exact continuous_id.mul continuous_const

Continuous Scalar Multiplication under Commuting Actions

Informal description

Let $R$ and $A$ be types, where $A$ is a monoid with a scalar multiplication action by $R$ such that the actions of $R$ and $A$ on $A$ commute (i.e., $r \cdot (a \cdot b) = a \cdot (r \cdot b)$ for all $r \in R$ and $a, b \in A$). If $A$ is equipped with a topological space structure and has continuous multiplication, then the scalar multiplication by any fixed element of $R$ is continuous in $A$.

MulOpposite.instContinuousMul instance

[TopologicalSpace α] [Mul α] [ContinuousMul α] : ContinuousMul αᵐᵒᵖ

Full source

/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
@[to_additive "If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`."]
instance [TopologicalSpace α] [Mul α] [ContinuousMul α] : ContinuousMul αᵐᵒᵖ :=
  ⟨continuous_op.comp (continuous_unop.snd'.mul continuous_unop.fst')⟩

Continuity of Multiplication in the Opposite Monoid

Informal description

For any topological space $\alpha$ with a multiplication operation that is continuous, the opposite monoid $\alpha^{\text{op}}$ also has a continuous multiplication operation.

Units.instContinuousMul instance

: ContinuousMul αˣ

Full source

/-- If multiplication on a monoid is continuous, then multiplication on the units of the monoid,
with respect to the induced topology, is continuous.

Inversion is also continuous, but we register this in a later file, `Topology.Algebra.Group`,
because the predicate `ContinuousInv` has not yet been defined. -/
@[to_additive "If addition on an additive monoid is continuous, then addition on the additive units
of the monoid, with respect to the induced topology, is continuous.

Negation is also continuous, but we register this in a later file, `Topology.Algebra.Group`, because
the predicate `ContinuousNeg` has not yet been defined."]
instance : ContinuousMul αˣ := isInducing_embedProduct.continuousMul (embedProduct α)

Continuous Multiplication on the Group of Units

Informal description

For any topological monoid $\alpha$ with continuous multiplication, the group of units $\alpha^\times$ also has continuous multiplication with respect to the induced topology.

Continuous.units_map theorem

 [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N] (f : M →* N) (hf : Continuous f) :
  Continuous (Units.map f)

Full source

@[to_additive (attr := fun_prop)]
theorem Continuous.units_map [Monoid M] [Monoid N] [TopologicalSpace M] [TopologicalSpace N]
    (f : M →* N) (hf : Continuous f) : Continuous (Units.map f) :=
  Units.continuous_iff.2 ⟨hf.comp Units.continuous_val, hf.comp Units.continuous_coe_inv⟩

Continuity of the Induced Map on Units of Continuous Monoid Homomorphisms

Informal description

Let $M$ and $N$ be monoids equipped with topological spaces, and let $f: M \to N$ be a continuous monoid homomorphism. Then the induced map $f^\times: M^\times \to N^\times$ on the groups of units is continuous, where $M^\times$ and $N^\times$ are equipped with their induced topologies.

Submonoid.mem_nhds_one theorem

(S : Submonoid M) (oS : IsOpen (S : Set M)) : (S : Set M) ∈ 𝓝 (1 : M)

Full source

@[to_additive]
theorem Submonoid.mem_nhds_one (S : Submonoid M) (oS : IsOpen (S : Set M)) :
    (S : Set M) ∈ 𝓝 (1 : M) :=
  IsOpen.mem_nhds oS S.one_mem

Open Submonoid Contains Identity in its Neighborhood

Informal description

For any open submonoid $S$ of a topological monoid $M$, the set $S$ is a neighborhood of the identity element $1 \in M$.

tendsto_multiset_prod theorem

 {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
  (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => (s.map fun c => f c b).prod) x (𝓝 (s.map a).prod)

Full source

@[to_additive]
theorem tendsto_multiset_prod {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Multiset ι) :
    (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
      Tendsto (fun b => (s.map fun c => f c b).prod) x (𝓝 (s.map a).prod) := by
  rcases s with ⟨l⟩
  simpa using tendsto_list_prod l

Limit of Product of Functions Indexed by a Multiset in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $\{f_i : \alpha \to M\}_{i \in \iota}$ a family of functions, $x$ a filter on $\alpha$, and $\{a_i\}_{i \in \iota}$ a family of points in $M$. For any multiset $s$ of indices in $\iota$, if for each $i \in s$ the function $f_i$ tends to $a_i$ along the filter $x$, then the product $\prod_{i \in s} f_i(b)$ tends to $\prod_{i \in s} a_i$ along $x$ as $b$ varies.

tendsto_finset_prod theorem

 {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
  (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))

Full source

@[to_additive]
theorem tendsto_finset_prod {f : ι → α → M} {x : Filter α} {a : ι → M} (s : Finset ι) :
    (∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))) →
      Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c)) :=
  tendsto_multiset_prod _

Limit of Finite Product of Functions in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $\{f_i : \alpha \to M\}_{i \in \iota}$ a family of functions, $x$ a filter on $\alpha$, and $\{a_i\}_{i \in \iota}$ a family of points in $M$. For any finite set $s$ of indices in $\iota$, if for each $i \in s$ the function $f_i$ tends to $a_i$ along the filter $x$, then the product $\prod_{i \in s} f_i(b)$ tends to $\prod_{i \in s} a_i$ along $x$ as $b$ varies.

continuous_multiset_prod theorem

 {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (s.map fun i => f i a).prod

Full source

@[to_additive (attr := continuity)]
theorem continuous_multiset_prod {f : ι → X → M} (s : Multiset ι) :
    (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (s.map fun i => f i a).prod := by
  rcases s with ⟨l⟩
  simpa using continuous_list_prod l

Continuity of Finite Products of Continuous Functions Indexed by a Multiset in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $X$ a topological space, and $\{f_i : X \to M\}_{i \in \iota}$ a family of functions. For any multiset $s$ of indices in $\iota$, if each function $f_i$ with $i \in s$ is continuous, then the product function $a \mapsto \prod_{i \in s} f_i(a)$ is continuous on $X$.

continuousOn_multiset_prod theorem

 {f : ι → X → M} (s : Multiset ι) {t : Set X} :
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (s.map fun i => f i a).prod) t

Full source

@[to_additive]
theorem continuousOn_multiset_prod {f : ι → X → M} (s : Multiset ι) {t : Set X} :
    (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => (s.map fun i => f i a).prod) t := by
  rcases s with ⟨l⟩
  simpa using continuousOn_list_prod l

Continuity of Product of Functions on a Subset in a Topological Monoid for Multisets

Informal description

Let $M$ be a topological monoid, $\{f_i : X \to M\}_{i \in \iota}$ a family of functions, and $t \subseteq X$. For any multiset $s$ of indices in $\iota$, if each function $f_i$ for $i \in s$ is continuous on $t$, then the product function $\prod_{i \in s} f_i$ is continuous on $t$.

continuous_finset_prod theorem

{f : ι → X → M} (s : Finset ι) : (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_finset_prod {f : ι → X → M} (s : Finset ι) :
    (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a :=
  continuous_multiset_prod _

Continuity of Finite Products of Continuous Functions Indexed by a Finite Set in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $X$ a topological space, and $\{f_i : X \to M\}_{i \in \iota}$ a family of functions. For any finite set $s$ of indices in $\iota$, if each function $f_i$ with $i \in s$ is continuous, then the product function $a \mapsto \prod_{i \in s} f_i(a)$ is continuous on $X$.

continuousOn_finset_prod theorem

 {f : ι → X → M} (s : Finset ι) {t : Set X} : (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t

Full source

@[to_additive]
theorem continuousOn_finset_prod {f : ι → X → M} (s : Finset ι) {t : Set X} :
    (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => ∏ i ∈ s, f i a) t :=
  continuousOn_multiset_prod _

Continuity of Finite Product of Functions on a Subset in a Topological Monoid

Informal description

Let $M$ be a topological monoid, $X$ a topological space, $\{f_i : X \to M\}_{i \in \iota}$ a family of functions, and $t \subseteq X$. For any finite set $s \subseteq \iota$, if each function $f_i$ with $i \in s$ is continuous on $t$, then the product function $a \mapsto \prod_{i \in s} f_i(a)$ is continuous on $t$.

eventuallyEq_prod theorem

 {X M : Type*} [CommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) :
  ∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i

Full source

@[to_additive]
theorem eventuallyEq_prod {X M : Type*} [CommMonoid M] {s : Finset ι} {l : Filter X}
    {f g : ι → X → M} (hs : ∀ i ∈ s, f i =ᶠ[l] g i) : ∏ i ∈ s, f i∏ i ∈ s, f i =ᶠ[l] ∏ i ∈ s, g i := by
  replace hs : ∀ᶠ x in l, ∀ i ∈ s, f i x = g i x := by rwa [eventually_all_finset]
  filter_upwards [hs] with x hx
  simp only [Finset.prod_apply, Finset.prod_congr rfl hx]

Eventual Equality of Finite Products under Componentwise Eventual Equality

Informal description

Let $M$ be a commutative monoid, $X$ a type, $s$ a finite subset of indices, $l$ a filter on $X$, and $f, g : \iota \to X \to M$ two families of functions. If for every $i \in s$, the functions $f_i$ and $g_i$ are eventually equal with respect to the filter $l$, then the finite products $\prod_{i \in s} f_i$ and $\prod_{i \in s} g_i$ are also eventually equal with respect to $l$. In symbols: $$\left(\forall i \in s, f_i =^l g_i\right) \implies \left(\prod_{i \in s} f_i =^l \prod_{i \in s} g_i\right)$$

LocallyFinite.exists_finset_mulSupport theorem

 {M : Type*} [One M] {f : ι → X → M} (hf : LocallyFinite fun i => mulSupport <| f i) (x₀ : X) :
  ∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ I

Full source

@[to_additive]
theorem LocallyFinite.exists_finset_mulSupport {M : Type*} [One M] {f : ι → X → M}
    (hf : LocallyFinite fun i => mulSupport <| f i) (x₀ : X) :
    ∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, (mulSupport fun i => f i x) ⊆ I := by
  rcases hf x₀ with ⟨U, hxU, hUf⟩
  refine ⟨hUf.toFinset, mem_of_superset hxU fun y hy i hi => ?_⟩
  rw [hUf.coe_toFinset]
  exact ⟨y, hi, hy⟩

Existence of Finite Multiplicative Support for Locally Finite Family of Functions

Informal description

Let $M$ be a type with a distinguished element $1$, and let $f : \iota \to X \to M$ be a family of functions. Suppose that the collection of multiplicative supports $\{\text{mulSupport}(f_i)\}_{i \in \iota}$ is locally finite. Then for any point $x_0 \in X$, there exists a finite subset $I \subseteq \iota$ such that for all $x$ in some neighborhood of $x_0$, the multiplicative support of the function $i \mapsto f_i(x)$ is contained in $I$.

finprod_eventually_eq_prod theorem

 {M : Type*} [CommMonoid M] {f : ι → X → M} (hf : LocallyFinite fun i => mulSupport (f i)) (x : X) :
  ∃ s : Finset ι, ∀ᶠ y in 𝓝 x, ∏ᶠ i, f i y = ∏ i ∈ s, f i y

Full source

@[to_additive]
theorem finprod_eventually_eq_prod {M : Type*} [CommMonoid M] {f : ι → X → M}
    (hf : LocallyFinite fun i => mulSupport (f i)) (x : X) :
    ∃ s : Finset ι, ∀ᶠ y in 𝓝 x, ∏ᶠ i, f i y = ∏ i ∈ s, f i y :=
  let ⟨I, hI⟩ := hf.exists_finset_mulSupport x
  ⟨I, hI.mono fun _ hy => finprod_eq_prod_of_mulSupport_subset _ fun _ hi => hy hi⟩

Local Equality of Finitary and Finite Products in Commutative Monoids

Informal description

Let $M$ be a commutative monoid and $f : \iota \to X \to M$ be a family of functions such that the collection of multiplicative supports $\{\text{mulSupport}(f_i)\}_{i \in \iota}$ is locally finite. Then for any point $x \in X$, there exists a finite subset $s \subseteq \iota$ such that for all $y$ in some neighborhood of $x$, the finitary product $\prod_{i} f_i(y)$ equals the finite product $\prod_{i \in s} f_i(y)$.

continuous_finprod theorem

 {f : ι → X → M} (hc : ∀ i, Continuous (f i)) (hf : LocallyFinite fun i => mulSupport (f i)) :
  Continuous fun x => ∏ᶠ i, f i x

Full source

@[to_additive]
theorem continuous_finprod {f : ι → X → M} (hc : ∀ i, Continuous (f i))
    (hf : LocallyFinite fun i => mulSupport (f i)) : Continuous fun x => ∏ᶠ i, f i x := by
  refine continuous_iff_continuousAt.2 fun x => ?_
  rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
  refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)
  exact tendsto_finset_prod _ fun i _ => (hc i).continuousAt

Continuity of Finitary Product of Continuous Functions with Locally Finite Support

Informal description

Let $M$ be a topological commutative monoid and $f : \iota \to X \to M$ a family of continuous functions such that the collection of multiplicative supports $\{\text{mulSupport}(f_i)\}_{i \in \iota}$ is locally finite. Then the function $x \mapsto \prod_{i} f_i(x)$ is continuous.

continuous_finprod_cond theorem

 {f : ι → X → M} {p : ι → Prop} (hc : ∀ i, p i → Continuous (f i)) (hf : LocallyFinite fun i => mulSupport (f i)) :
  Continuous fun x => ∏ᶠ (i) (_ : p i), f i x

Full source

@[to_additive]
theorem continuous_finprod_cond {f : ι → X → M} {p : ι → Prop} (hc : ∀ i, p i → Continuous (f i))
    (hf : LocallyFinite fun i => mulSupport (f i)) :
    Continuous fun x => ∏ᶠ (i) (_ : p i), f i x := by
  simp only [← finprod_subtype_eq_finprod_cond]
  exact continuous_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)

Continuity of Conditional Finitary Product of Continuous Functions with Locally Finite Support

Informal description

Let $M$ be a topological commutative monoid and $f : \iota \to X \to M$ a family of functions such that for each $i \in \iota$ satisfying a predicate $p(i)$, the function $f_i$ is continuous. If the collection of multiplicative supports $\{\text{mulSupport}(f_i)\}_{i \in \iota}$ is locally finite, then the function $x \mapsto \prod_{i \in \iota, p(i)} f_i(x)$ is continuous.

instContinuousAddAdditiveOfContinuousMul instance

[TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousAdd (Additive M)

Full source

instance [TopologicalSpace M] [Mul M] [ContinuousMul M] : ContinuousAdd (Additive M) where
  continuous_add := @continuous_mul M _ _ _

Continuous Addition in the Additive Version of a Continuous Multiplicative Monoid

Informal description

For any topological space $M$ with a multiplication operation that is continuous (i.e., the multiplication map $M \times M \to M$ is continuous), the additive version of $M$ (where multiplication is reinterpreted as addition) inherits a continuous addition operation.

instContinuousMulMultiplicativeOfContinuousAdd instance

[TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousMul (Multiplicative M)

Full source

instance [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousMul (Multiplicative M) where
  continuous_mul := @continuous_add M _ _ _

Continuous Multiplication in the Multiplicative Version of a Continuous Additive Structure

Informal description

For any type $M$ with an addition operation and a topology such that addition is continuous, the multiplicative version of $M$ (where addition is interpreted as multiplication) also has continuous multiplication.

continuousMul_sInf theorem

{ts : Set (TopologicalSpace M)} (h : ∀ t ∈ ts, @ContinuousMul M t _) : @ContinuousMul M (sInf ts) _

Full source

@[to_additive]
theorem continuousMul_sInf {ts : Set (TopologicalSpace M)}
    (h : ∀ t ∈ ts, @ContinuousMul M t _) : @ContinuousMul M (sInf ts) _ :=
  letI := sInf ts
  { continuous_mul :=
      continuous_sInf_rng.2 fun t ht =>
        continuous_sInf_dom₂ ht ht (@ContinuousMul.continuous_mul M t _ (h t ht)) }

Continuity of Multiplication under Infimum Topology

Informal description

Let $M$ be a type with a multiplication operation, and let $\{t_i\}_{i \in I}$ be a set of topologies on $M$ such that for each $i \in I$, the multiplication on $M$ is continuous with respect to $t_i$. Then the multiplication is also continuous with respect to the infimum topology $\bigwedge_{i \in I} t_i$.

continuousMul_iInf theorem

{ts : ι' → TopologicalSpace M} (h' : ∀ i, @ContinuousMul M (ts i) _) : @ContinuousMul M (⨅ i, ts i) _

Full source

@[to_additive]
theorem continuousMul_iInf {ts : ι' → TopologicalSpace M}
    (h' : ∀ i, @ContinuousMul M (ts i) _) : @ContinuousMul M (⨅ i, ts i) _ := by
  rw [← sInf_range]
  exact continuousMul_sInf (Set.forall_mem_range.mpr h')

Continuity of Multiplication under Infimum of Topologies

Informal description

Let $M$ be a type with a multiplication operation, and let $\{t_i\}_{i \in \iota'}$ be a family of topologies on $M$ indexed by $\iota'$ such that for each $i \in \iota'$, the multiplication on $M$ is continuous with respect to $t_i$. Then the multiplication is also continuous with respect to the infimum topology $\bigwedge_{i \in \iota'} t_i$.

continuousMul_inf theorem

 {t₁ t₂ : TopologicalSpace M} (h₁ : @ContinuousMul M t₁ _) (h₂ : @ContinuousMul M t₂ _) : @ContinuousMul M (t₁ ⊓ t₂) _

Full source

@[to_additive]
theorem continuousMul_inf {t₁ t₂ : TopologicalSpace M} (h₁ : @ContinuousMul M t₁ _)
    (h₂ : @ContinuousMul M t₂ _) : @ContinuousMul M (t₁ ⊓ t₂) _ := by
  rw [inf_eq_iInf]
  refine continuousMul_iInf fun b => ?_
  cases b <;> assumption

Continuity of Multiplication under Infimum of Two Topologies

Informal description

Let $M$ be a type with a multiplication operation, and let $t_1$ and $t_2$ be two topologies on $M$ such that the multiplication is continuous with respect to both $t_1$ and $t_2$. Then the multiplication is also continuous with respect to the infimum topology $t_1 \sqcap t_2$.

ContinuousMap.mulRight definition

(x : X) : C(X, X)

Full source

/-- The continuous map `fun y => y * x` -/
@[to_additive "The continuous map `fun y => y + x`"]
protected def mulRight (x : X) : C(X, X) :=
  mk _ (continuous_mul_right x)

Continuous right multiplication map

Informal description

For a topological space $ X $ with a continuous multiplication operation, the function $ \text{ContinuousMap.mulRight} $ takes an element $ x \in X $ and returns the continuous map $ y \mapsto y * x $ from $ X $ to itself.

ContinuousMap.coe_mulRight theorem

(x : X) : ⇑(ContinuousMap.mulRight x) = fun y => y * x

Full source

@[to_additive (attr := simp)]
theorem coe_mulRight (x : X) : ⇑(ContinuousMap.mulRight x) = fun y => y * x :=
  rfl

Underlying function of continuous right multiplication map

Informal description

For any element $x$ in a topological space $X$ with a continuous multiplication operation, the underlying function of the continuous right multiplication map $\text{ContinuousMap.mulRight}(x)$ is given by $y \mapsto y * x$.

ContinuousMap.mulLeft definition

(x : X) : C(X, X)

Full source

/-- The continuous map `fun y => x * y` -/
@[to_additive "The continuous map `fun y => x + y`"]
protected def mulLeft (x : X) : C(X, X) :=
  mk _ (continuous_mul_left x)

Left multiplication as a continuous map

Informal description

For any element $ x $ in a topological space $ X $ with a continuous multiplication operation, the function $ \text{ContinuousMap.mulLeft} $ maps $ x $ to the continuous function $ y \mapsto x * y $ from $ X $ to itself.

ContinuousMap.coe_mulLeft theorem

(x : X) : ⇑(ContinuousMap.mulLeft x) = fun y => x * y

Full source

@[to_additive (attr := simp)]
theorem coe_mulLeft (x : X) : ⇑(ContinuousMap.mulLeft x) = fun y => x * y :=
  rfl

Underlying function of continuous left multiplication map

Informal description

For any element $x$ in a topological space $X$ with a continuous multiplication operation, the underlying function of the continuous left multiplication map $\text{ContinuousMap.mulLeft}(x)$ is given by $y \mapsto x * y$.