FilteredFamilies.lean

theorem directed_finset_has_lower_bound {α : Type*} {ι : Type*} {U : ι → Set α}
    (hdir : Directed (· ⊇ ·) U) :
    ∀ s : Finset ι, s.Nonempty → ∃ k : ι, ∀ i ∈ s, U k ⊆ U i

theorem closedSubgroup_mul_iInter_eq_iInter_mul [CompactSpace G]
    (H : ClosedSubgroup G) {ι : Type v} (U : ι → Set G)
    (hclosed : ∀ i, IsClosed (U i))
    (hdir : Directed (· ⊇ ·) U) :
    ((H : Set G) * ⋂ i, U i) = ⋂ i, ((H : Set G) * U i)

theorem continuous_surjective_image_iInter_eq_iInter_image {X : Type u}
    [TopologicalSpace X] [CompactSpace X] {R : Type v} [TopologicalSpace R] [T2Space R]
    (φ : X → R) (hφ : Continuous φ) (hsurj : Function.Surjective φ)
    {ι : Type w} (U : ι → Set X)
    (hclosed : ∀ i, IsClosed (U i))
    (hdir : Directed (· ⊇ ·) U) :
    φ '' ⋂ i, U i = ⋂ i, φ '' U i

theorem exists_openNormalSubgroup_mul_subset_openSubgroup [CompactSpace G]
    (H : ClosedSubgroup G) (V : OpenSubgroup G)
    (hHV : (H : Subgroup G) ≤ (V : Subgroup G)) :
    ∃ U : OpenNormalSubgroup G, ((H : Set G) * (U : Set G)) ⊆ (V : Set G)

theorem closedSubgroup_eq_sInf_openNormal [CompactSpace G] [TotallyDisconnectedSpace G]
    (H : ClosedSubgroup G) [((H : Subgroup G).Normal)] :
    (H : Subgroup G) =
      sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N ∧ N.Normal}

theorem finite_iInter_subgroup_subset_openSubgroup [CompactSpace G] {ι : Type v}
    (H : ι → Subgroup G)
    (hclosed : ∀ i, IsClosed (((H i : Subgroup G) : Set G)))
    (U : OpenSubgroup G)
    (hInter : (⋂ i, (((H i : Subgroup G) : Set G))) ⊆ (((U : Subgroup G) : Set G))) :
    ∃ s : Finset ι, (⋂ i ∈ s, (((H i : Subgroup G) : Set G))) ⊆ (((U : Subgroup G) : Set G))

theorem finite_openSubgroup_intersections_form_nhds_basis [CompactSpace G]
    [IsTopologicalGroup G] [TotallyDisconnectedSpace G] {ι : Type v} (U : ι → OpenSubgroup G)
    (hInter : (⋂ i, (((U i : Subgroup G) : Set G))) = ({1} : Set G)) :
    ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
      ∃ s : Finset ι, (⋂ i ∈ s, (((U i : Subgroup G) : Set G))) ⊆ W