Theorems · Theorem · general topology

ShrinkingLemma.PartialRefinement.find_apply_of_mem

∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  {c : Set (ShrinkingLemma.PartialRefinement u s p)},
  IsChain (fun x1 x2 => x1 ≤ x2) c →
    ∀ (ne : c.Nonempty) {i : ι} {v : ShrinkingLemma.PartialRefinement u s p},
      v ∈ c → i ∈ v.carrier → (ShrinkingLemma.PartialRefinement.find c ne i).toFun i = v.toFun i

Defined in

Mathlib.Topology.ShrinkingLemma

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace