isOpen_of_isOpen — Mathlib

English

If a set in E is open in the weak topology, then it is open in the original topology.

Русский

Если множество в E открыто в слабой топологии, то оно открыто и в исходной топологии.

LaTeX

$$$IsOpen((toWeakSpaceCLM 𝕜 E)''V) \\Rightarrow IsOpen\\ V$$$

Lean4

/-- A set in `E` which is open in the weak topology is open. -/
theorem isOpen_of_isOpen (V : Set E) (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
  simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV

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