Theorems · Definition · general topology

Filter.Realizer.mk.noConfusion

{α : Type u_1} →
  {f : Filter α} →
    {P : Sort u} →
      {σ : Type u_5} →
        {F : CFilter (Set α) σ} →
          {eq : F.toFilter = f} →
            {σ' : Type u_5} →
              {F' : CFilter (Set α) σ'} →
                {eq' : F'.toFilter = f} →
                  { σ := σ, F := F, eq := eq } = { σ := σ', F := F', eq := eq' } → (σ = σ' → F ≍ F' → P) → P

Defined in

Mathlib.Data.Analysis.Filter

Cited by

1 results in Mathlib

Foundations

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