smul_right

Mathlib.Topology.Algebra.FilterBasis

URI: https://scilib.ai/kg/mathlib#ModuleFilterBasis.smul_right

English

For any m0 ∈ M and U ∈ BM there exists V ∈ BM with V ⊆ { x ∈ M | x · m0 ∈ U }.

Русский

Для любого m0 ∈ M и U ∈ BM существует V ∈ BM, такой что V ⊆ { x ∈ M | x · m0 ∈ U }.

LaTeX

$$$\exists V\in BM, V \subseteq (\lambda x \mapsto x · m_0)^{-1}' U$.$$

Lean4

theorem smul_right (m₀ : M) {U : Set M} (hU : U ∈ B) : ∀ᶠ x in 𝓝 (0 : R), x • m₀ ∈ U :=
  B.smul_right' m₀ hU

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

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

Разделы

Аффилиация

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