English
Let E be equipped with a bilinear form B: E × F → 𝕜. The space E is endowed with the weak topology induced by B, i.e., the initial topology on E with respect to the family of maps x ↦ B(x, y) for all y in F (equivalently, the coarsest topology making each x ↦ B(x, y) continuous).
Русский
Пусть имеется билинейная форма B: E × F → 𝕜. Пространство E наделяют слабой топологией, индуцированной B, то есть начальной топологией на E по семейству отображений x ↦ B(x, y) для всех y ∈ F (то есть наименьшей топологией, при которой каждое x ↦ B(x, y) непрерывно).
LaTeX
$$$\\tau_{B}$ равно начальной топологии на $E$ относительно семейства отображений $x \\mapsto B(x,y)$ ($y \\in F$), т.е. топология на $E$ такая, что $B(-,y): E \\to \\mathbb{k}$ непрерывны для всех $y\\in F$.$$
Lean4
/-- The space `E` equipped with the weak topology induced by the bilinear form `B`. -/
@[nolint unusedArguments]
def WeakBilin [CommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (_ : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :=
E
deriving AddCommMonoid, Module 𝕜
