Theorems · Definition · global analysis

DiffeologicalSpace.noConfusion

{P : Sort u} →
  {X : Type u_1} →
    {t : DiffeologicalSpace X} →
      {X' : Type u_1} → {t' : DiffeologicalSpace X'} → X = X' → t ≍ t' → DiffeologicalSpace.noConfusionType P t t'

Defined in

Mathlib.Geometry.Diffeology.Basic

Cited by

0 results in Mathlib

Foundations

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