Theorems · Theorem · general topology

Filter.GenerateSets.brecOn

∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {a : Set α}
  (t : Filter.GenerateSets g a),
  (∀ (a : Set α) (t : Filter.GenerateSets g a), Filter.GenerateSets.below t → motive a 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