Theorems · Definition · general topology

Filter.IsCountableBasis.recOn

{α : Type u_1} →
  {ι : Type u_4} →
    {p : ι → Prop} →
      {s : ι → Set α} →
        {motive : Filter.IsCountableBasis p s → Sort u} →
          (t : Filter.IsCountableBasis p s) →
            ((toIsBasis : Filter.IsBasis p s) → (countable : (Set.ofPred p).Countable) → motive ⋯) → motive t

Defined in

Mathlib.Order.Filter.CountablyGenerated

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms