isOpen_deltaGenerated_iff — Mathlib

English

A subset u of X is open in deltaGenerated X iff all its preimages under finite-dimensional continuous maps are open.

Русский

Подмножество u пространства X открыто в deltaGenerated X тогда и только тогда, когда все его прообрази по непрерывным отображениям из конечномерного Евклида открыты.

LaTeX

$$$\\text{IsOpen}[\\deltaGenerated X]\,u \\iff \\forall n\\; \\forall p: C(Fin n \\to \\mathbb{R}, X), \\ IsOpen(p^{-1} u)$$$

Lean4

/-- A set is open in `deltaGenerated X` iff all its preimages under continuous functions ℝⁿ → X are
  open. -/
theorem isOpen_deltaGenerated_iff {u : Set X} :
    IsOpen[deltaGenerated X] u ↔ ∀ n (p : C(Fin n → ℝ, X)), IsOpen (p ⁻¹' u) := by
  simp_rw [deltaGenerated, isOpen_iSup_iff, isOpen_coinduced, Sigma.forall]

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