import Mathlib.Topology.AlexandrovDiscrete

/-!
# Sheaf Mathematical Institute · result 1

Source: J. Widman, *Topology and Sheaf Cohomology in Finite Topological Spaces* (2026),
Lemma 5.1: on a finite space, every open cover of the minimal open set `U_x` around a point `x`
contains a member equal to `U_x`.

In mathlib the intersection of all open sets containing `x` is `nhdsKer {x}`. It is open exactly
when the space is Alexandrov-discrete, and every finite space is (`Finite.toAlexandrovDiscrete`),
so in the paper's setting `nhdsKer {x}` is the minimal open set `U_x`.

The formalisation showed the covering statement needs no finiteness at all: it holds in every
topological space, because `nhdsKer {x}` is contained in every open set containing `x`. The
paper's hypothesis is only what makes `nhdsKer {x}` itself open. Both facts are recorded below.
-/

open Set

/-- **Lemma 5.1, general form.** In any topological space, if open sets `V i` cover
`nhdsKer {x}` (the intersection of all open sets containing `x`), then one of them equals it. -/
theorem exists_eq_nhdsKer_singleton_of_cover {X : Type*} [TopologicalSpace X] {ι : Type*}
    (x : X) (V : ι → Set X) (hV : ∀ i, IsOpen (V i)) (hcov : nhdsKer {x} = ⋃ i, V i) :
    ∃ i, V i = nhdsKer {x} := by
  -- `x` lies in `nhdsKer {x}`, hence in some member of the cover
  have hx : x ∈ nhdsKer ({x} : Set X) := subset_nhdsKer (mem_singleton x)
  rw [hcov] at hx
  obtain ⟨i, hi⟩ := mem_iUnion.mp hx
  refine ⟨i, subset_antisymm ?_ ?_⟩
  · -- `V i ⊆ ⋃ j, V j = nhdsKer {x}`
    rw [hcov]; exact subset_iUnion V i
  · -- `nhdsKer {x}` is contained in every open set containing `x`, and `V i` is one
    exact nhdsKer_minimal (singleton_subset_iff.mpr hi) (hV i)

/-- **Lemma 5.1 as stated in the paper.** In a finite space `U_x = nhdsKer {x}` is open, so it is
the smallest open set containing `x`, and every open cover of it contains `U_x` itself. -/
theorem FiniteSpace.minimal_open_isOpen_and_exists_eq_of_cover {X : Type*} [TopologicalSpace X]
    [Finite X] {ι : Type*} (x : X) (V : ι → Set X) (hV : ∀ i, IsOpen (V i))
    (hcov : nhdsKer {x} = ⋃ i, V i) :
    IsOpen (nhdsKer ({x} : Set X)) ∧ ∃ i, V i = nhdsKer {x} :=
  ⟨isOpen_nhdsKer, exists_eq_nhdsKer_singleton_of_cover x V hV hcov⟩