Grace/Cumulus/Topology/FiniteIntersection.g17

Open in Workbench Download source

Imports

Space · Cardinal.ListSupport

Declarations

Source

1-- Finitely many open sets intersect in an open set2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Topology.FiniteIntersection8import Space9import Cardinal.ListSupport1011theorem IsTopology.list_intersection (X T : Set) (xs : List(T))12  requires topology : IsTopology(X, T)13  requires inhabited : Nonempty(listSupport{T}(xs))14  shows ⋂(listSupport{T}(xs)) ∈ T15proof16  induction xs17  | List.nil =>18    intro inhabited19    exfalso20    rw listSupport.nil at inhabited21    obtain ⟨x, hx⟩ := inhabited22    exact empty.membership with x, hx23  | List.cons(a, tail) using ih =>24    intro inhabited25    have element : a ∈ T by assumption26    rw listSupport.cons27    have self : a ∈ {a} by simp [singleton.membership]28    have singletonInhabited : Nonempty({a}) := ⟨a, self⟩29    have split : Nonempty(listSupport{T}(tail)) ∨ ¬Nonempty(listSupport{T}(tail)) by tauto30    cases split with some | none31    . have inner := ih with some32      have joined := familyIntersection.union2 with singletonInhabited, some33      unfold insert34      rw [joined, familyIntersection.singleton]35      exact IsTopology.intersection2 with topology, element, inner36    . have empty : listSupport{T}(tail) = ∅37        by_contra different38        apply none39        exact Nonempty.of_ne_empty with different40      unfold insert41      rwa [empty, union2.right_empty, familyIntersection.singleton]4243theorem IsTopology.finite_intersection (X T F : Set)44  requires topology : IsTopology(X, T)45  requires finite : Finite(F)46  requires inside : F ⊆ T47  requires inhabited : Nonempty(F)48  shows ⋂(F) ∈ T49proof50  obtain ⟨xs, list, covers⟩ := Finite.list_cover with finite51  have weakened := List.weaken with inside52  have support := listSupport.subset with list53  have equal : listSupport{F}(xs) = F54    apply Subset.antisymmetric55    . exact support56    . exact covers57  have carrier := listSupport.change_carrier with inside58  rw carrier at equal59  rw ← equal60  rw ← equal at inhabited61  exact IsTopology.list_intersection with topology, inhabited62