-- Finitely many open sets intersect in an open set
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Topology.FiniteIntersection
import Space
import Cardinal.ListSupport

theorem IsTopology.list_intersection (X T : Set) (xs : List(T))
  requires topology : IsTopology(X, T)
  requires inhabited : Nonempty(listSupport{T}(xs))
  shows ⋂(listSupport{T}(xs)) ∈ T
proof
  induction xs
  | List.nil =>
    intro inhabited
    exfalso
    rw listSupport.nil at inhabited
    obtain ⟨x, hx⟩ := inhabited
    exact empty.membership with x, hx
  | List.cons(a, tail) using ih =>
    intro inhabited
    have element : a ∈ T by assumption
    rw listSupport.cons
    have self : a ∈ {a} by simp [singleton.membership]
    have singletonInhabited : Nonempty({a}) := ⟨a, self⟩
    have split : Nonempty(listSupport{T}(tail)) ∨ ¬Nonempty(listSupport{T}(tail)) by tauto
    cases split with some | none
    . have inner := ih with some
      have joined := familyIntersection.union2 with singletonInhabited, some
      unfold insert
      rw [joined, familyIntersection.singleton]
      exact IsTopology.intersection2 with topology, element, inner
    . have empty : listSupport{T}(tail) = ∅
        by_contra different
        apply none
        exact Nonempty.of_ne_empty with different
      unfold insert
      rwa [empty, union2.right_empty, familyIntersection.singleton]

theorem IsTopology.finite_intersection (X T F : Set)
  requires topology : IsTopology(X, T)
  requires finite : Finite(F)
  requires inside : F ⊆ T
  requires inhabited : Nonempty(F)
  shows ⋂(F) ∈ T
proof
  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite
  have weakened := List.weaken with inside
  have support := listSupport.subset with list
  have equal : listSupport{F}(xs) = F
    apply Subset.antisymmetric
    . exact support
    . exact covers
  have carrier := listSupport.change_carrier with inside
  rw carrier at equal
  rw ← equal
  rw ← equal at inhabited
  exact IsTopology.list_intersection with topology, inhabited