mul

Mathlib.Topology.Algebra.FilterBasis

URI: https://scilib.ai/kg/mathlib#GroupFilterBasis.mul

English

For any U ∈ B there exists V ∈ B with V · V ⊆ U.

Русский

Для любого U ∈ B существует V ∈ B такое, что V · V ⊆ U.

LaTeX

$$U \in B \Rightarrow \exists V \in B, V \cdot V \subseteq U$$

Lean4

@[to_additive]
theorem mul {U : Set G} : U ∈ B → ∃ V ∈ B, V * V ⊆ U :=
  GroupFilterBasis.mul'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru