Theorems · Definition · global analysis

DiffeologicalSpace.casesOn

{X : Type u_1} →
  {motive : DiffeologicalSpace X → Sort u} →
    (t : DiffeologicalSpace X) →
      ((plots : (n : ℕ) → Set (EuclideanSpace ℝ (Fin n) → X)) →
          (constant_plots : ∀ {n : ℕ} (x : X), (fun x_1 => x) ∈ plots n) →
            (plot_reparam :
                ∀ {n m : ℕ} {p : EuclideanSpace ℝ (Fin m) → X}
                  {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)},
                  p ∈ plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots n) →
              (locality :
                  ∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
                    (∀ (x : EuclideanSpace ℝ (Fin n)),
                        ∃ u,
                          IsOpen u ∧
                            x ∈ u ∧
                              ∀ {m : ℕ} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
                                (∀ (x : EuclideanSpace ℝ (Fin m)), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots m) →
                      p ∈ plots n) →
                (dTopology : TopologicalSpace X) →
                  (isOpen_iff_preimages_plots :
                      ∀ {u : Set X}, TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, IsOpen (p ⁻¹' u)) →
                    motive
                      { plots := plots, constant_plots := constant_plots, plot_reparam := plot_reparam,
                        locality := locality, dTopology := dTopology,
                        isOpen_iff_preimages_plots := isOpen_iff_preimages_plots }) →
        motive t

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

1 results in Mathlib

Foundations

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