Equivalent_Definitions_of_Synthetic_Basis
Provedproofwikitopological-basestopology
Two definitions of a synthetic basis for a topology on X are equivalent.
Preamble
import Mathlib.Topology.Basic
Formal statement
theorem Equivalent_Definitions_of_Synthetic_Basis {X : Type _} (B : Set (Set X)) : (∀ A ∈ B, ∀ B_1 ∈ B, ∃ C : Set (Set X), C ⊆ B ∧ A ∩ B_1 = ⋃₀ C) ↔ (∀ A ∈ B, ∀ B_1 ∈ B, ∀ x ∈ A ∩ B_1, ∃ W ∈ B, x ∈ W ∧ W ⊆ A ∩ B_1) := by sorrySource