English
Let B be a bilinear form B: E →ₗ[𝕜] (F →ₗ[𝕜] 𝕜). Then the neighborhood basis at zero in the weak bilinear space WeakBilin(B) is generated by the seminorms coming from the seminorm family B.toSeminormFamily; equivalently, (nhds(0)) HasBasis B.toSeminormFamily.basisSets id.
Русский
Пусть B — билинейная форма B: E →ₗ[𝕜] (F →ₗ[𝕜] 𝕜). Тогда базис окрестностей нуля в слабом билиновом пространстве WeakBilin(B) порождается семинормами из семейства B.toSeminormFamily; эквивалентно, (nhds(0)) имеет базис B.toSeminormFamily.basisSets id.
LaTeX
$$$(\\nhds(0))\\;\\text{HasBasis } B.toSeminormFamily.basisSets\\; \\mathrm{id}$$$
Lean4
theorem hasBasis_weakBilin (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
(𝓝 (0 : WeakBilin B)).HasBasis B.toSeminormFamily.basisSets _root_.id :=
LinearMap.weakBilin_withSeminorms B |>.hasBasis
