Theorems · Definition · general topology

TopologicalSpace.GenerateOpen.recOn

∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} {a : Set α}
  (t : TopologicalSpace.GenerateOpen g a),
  (∀ (s : Set α) (a : s ∈ g), motive s ⋯) →
    motive Set.univ ⋯ →
      (∀ (s t : Set α) (a : TopologicalSpace.GenerateOpen g s) (a_1 : TopologicalSpace.GenerateOpen g t),
          motive s a → motive t a_1 → motive (s ∩ t) ⋯) →
        (∀ (S : Set (Set α)) (a : ∀ s ∈ S, TopologicalSpace.GenerateOpen g s),
            (∀ (s : Set α) (a_1 : s ∈ S), motive s ⋯) → motive (⋃₀ S) ⋯) →
          motive a t

Defined in

Mathlib.Topology.Order

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms