Theorems · Theorem · general topology

ShrinkingLemma.PartialRefinement.exists_gt

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} [NormalSpace X]
  (v : ShrinkingLemma.PartialRefinement u s ⊤), IsClosed s → ∀ i ∉ v.carrier, ∃ v', v < v'

If s is a closed set, v is a partial refinement, and i is an index such that i ∉ v.carrier, then there exists a partial refinement that is strictly greater than v.

Defined in

Mathlib.Topology.ShrinkingLemma

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpace