Theorems · Theorem · global analysis

DiffeologicalSpace.isOpen_iff_preimages_plots

∀ {X : Type u_1} [self : DiffeologicalSpace X] {u : Set X},
  TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ DiffeologicalSpace.plots n, IsOpen (p ⁻¹' u)

The D-topology consists of exactly those sets whose preimages under plots are all open.

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

1 results in Mathlib

Foundations

Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DiffeologicalSpace