Theorems · Definition · general topology

Filter.GenerateSets.casesOn

∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {a : Set α}
  (t : Filter.GenerateSets g a),
  (∀ {s : Set α} (a : s ∈ g), motive s ⋯) →
    motive Set.univ ⋯ →
      (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : s ⊆ t), motive t ⋯) →
        (∀ {s t : Set α} (a : Filter.GenerateSets g s) (a_1 : Filter.GenerateSets g t), motive (s ∩ t) ⋯) → motive a t

Defined in

Mathlib.Order.Filter.Basic

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms