smul — Mathlib

English

Let U ∈ BM. Then there exist V ∈ 𝓝(0) and W ∈ BM such that V · W ⊆ U; i.e., a small scalar neighborhood together with a basis element yields U.

Русский

Пусть U ∈ BM. Тогда существуют V ∈ 𝓝(0) и W ∈ BM такие, что V · W ⊆ U; то есть произведение малого окрестности скаляра и базисного элемента лежит в U.

LaTeX

$$$\exists V\in \mathcal{N}(0), \exists W\in BM, V \cdot W \subseteq U$.$$

Lean4

theorem smul {U : Set M} (hU : U ∈ B) : ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ B, V • W ⊆ U :=
  B.smul' hU

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