isOpen_iff — Mathlib

English

A subset u is open in deltaGenerated X iff for all n and all p: ContinuousMap(Fin n → Real, X), p^{-1}(u) is open.

Русский

Подмножество u открыто в deltaGenerated X тогда и только тогда, когда для всех n и всех p: ContinuousMap(Fin n → Real, X) прообраз p^{-1}(u) открыт.

LaTeX

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

Lean4

/-- A subset of a delta-generated space is open iff its preimage is open for every
  continuous map from ℝⁿ to X. -/
theorem isOpen_iff [DeltaGeneratedSpace X] {u : Set X} :
    IsOpen u ↔ ∀ (n : ℕ) (p : ContinuousMap ((Fin n) → ℝ) X), IsOpen (p ⁻¹' u) := by
  nth_rewrite 1 [eq_deltaGenerated (X := X)]; exact isOpen_deltaGenerated_iff

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