Commit 2024-01-16 09:52 be8dd312

View on Github →

feat(Topology/Basic): generalize to Sort*, add versions (#9753)

Generalize interior_iInter_of_finite and closure_iUnion_of_finite to functions from Sort*.
Add Set.Finite.interior_biInter, Set.Finite.interior_sInter, Set.Finite.closure_biUnion, and Set.Finite.closure_sUnion.
Move closure_eq_compl_interior_compl up to golf.

Estimated changes

Modified Mathlib/Topology/Basic.lean

added theorem Set.Finite.closure_biUnion

added theorem Set.Finite.closure_sUnion

added theorem Set.Finite.interior_biInter

added theorem Set.Finite.interior_sInter

modified theorem closure_iUnion_of_finite

modified theorem closure_union

modified theorem interior_iInter_of_finite