Commit 2023-02-05 18:01 25e60495

View on Github →

feat: port Topology.ShrinkingLemma (#2068)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/ShrinkingLemma.lean

added theorem ShrinkingLemma.PartialRefinement.apply_eq_of_chain

added def ShrinkingLemma.PartialRefinement.chainSup

added def ShrinkingLemma.PartialRefinement.chainSupCarrier

added theorem ShrinkingLemma.PartialRefinement.exists_gt

added def ShrinkingLemma.PartialRefinement.find

added theorem ShrinkingLemma.PartialRefinement.find_apply_of_mem

added theorem ShrinkingLemma.PartialRefinement.find_mem

added theorem ShrinkingLemma.PartialRefinement.le_chainSup

added theorem ShrinkingLemma.PartialRefinement.mem_find_carrier_iff

added structure ShrinkingLemma.PartialRefinement

added theorem exists_subset_unionᵢ_closed_subset

added theorem exists_subset_unionᵢ_closure_subset

added theorem exists_unionᵢ_eq_closed_subset

added theorem exists_unionᵢ_eq_closure_subset