continuous_mul_left — Mathlib

English

Left multiplication by a fixed ultrafilter on a semigroup is a continuous operation on the ultrafilter space.

Русский

Левое умножение на фиксированный ультрафильтр в полугруппе — непрерывная операция на пространстве ультрафильтров.

LaTeX

$$$\\\\text{Continuous}(x \\mapsto x * V) \\\\text{ on } Ultrafilter(M).$$$

Lean4

@[to_additive]
theorem continuous_mul_left {M} [Mul M] (V : Ultrafilter M) : Continuous (· * V) :=
  ultrafilterBasis_is_basis.continuous_iff.2 <|
    Set.forall_mem_range.mpr fun s ↦ ultrafilter_isOpen_basic {m : M | ∀ᶠ m' in V, m * m' ∈ s}

Похожие утверждения