Theorems · Definition · general topology

SpectralMap.noConfusion

{P : Sort u} →
  {α : Type u_6} →
    {β : Type u_7} →
      {inst : TopologicalSpace α} →
        {inst_1 : TopologicalSpace β} →
          {t : SpectralMap α β} →
            {α' : Type u_6} →
              {β' : Type u_7} →
                {inst' : TopologicalSpace α'} →
                  {inst'_1 : TopologicalSpace β'} →
                    {t' : SpectralMap α' β'} →
                      α = α' → β = β' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → SpectralMap.noConfusionType P t t'

Defined in: Mathlib.Topology.Spectral.Hom
Cited by: 0 results in Mathlib
Foundations: Depth 6 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
SpectralMapstatement and proof · cited by 20
IsSpectralMapproof · cited by 20
SpectralMap.noConfusionTypestatement · cited by 0
SpectralMap.casesOnproof · cited by 0

Cited by1

Results whose statement or proof uses this declaration.

SpectralMap.mk.noConfusionproof · cited by 1