instTopologicalSpace — Mathlib

English

Equip WeakBilin B with the topology induced by B, i.e., the topology on E is the induced topology via the map x ↦ (y ↦ B(x,y)) into the product space F → 𝕜 with the Pi topology.

Русский

Оборудуем WeakBilin B топологией, индуцированной B, то есть топологией на E, полученной как начальная по отображению x ↦ (y ↦ B(x,y)) в произведение F → 𝕜 с Pi-актовой топологией.

LaTeX

$$$\text{TopologicalSpace}(WeakBilin B) = \text{TopologicalSpace.induced}(f, \Pi{F}\mathbb{k})$ где $f(x)(y)=B(x,y)$.$$

Lean4

instance instTopologicalSpace : TopologicalSpace (WeakBilin B) :=
  TopologicalSpace.induced (fun x y => B x y) Pi.topologicalSpace

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