Theorems · Definition · general topology

Filter.Realizer.noConfusion

{P : Sort u} →
  {α : Type u_1} →
    {f : Filter α} →
      {t : f.Realizer} →
        {α' : Type u_1} →
          {f' : Filter α'} → {t' : f'.Realizer} → α = α' → f ≍ f' → t ≍ t' → Filter.Realizer.noConfusionType P t t'

Defined in

Mathlib.Data.Analysis.Filter

Cited by

0 results in Mathlib

Foundations

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