Theorems · Theorem · Lie groups

NonarchimedeanGroup.prod_self_subset

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [NonarchimedeanGroup G] {U : Set (G × G)},
  U ∈ nhds 1 → ∃ V, ↑V ×ˢ ↑V ⊆ U

An open neighborhood of the identity in the Cartesian square of a nonarchimedean group contains the Cartesian square of an open neighborhood in the group.

Defined in

Mathlib.Topology.Algebra.Nonarchimedean.Basic

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceNonarchimedeanGroup