smul_left

Mathlib.Topology.Algebra.FilterBasis

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

English

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

Русский

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

LaTeX

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

Lean4

theorem smul_left (x₀ : R) {U : Set M} (hU : U ∈ B) : ∃ V ∈ B, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U :=
  B.smul_left' x₀ hU

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

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

Разделы

Аффилиация

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