Theorems · Theorem · general topology

PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff

∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {x y : (n : ℕ) → E n}
  {s : Set ((n : ℕ) → E n)},
  IsClosed s →
    s.Nonempty →
      PiNat.longestPrefix x s < PiNat.firstDiff x y →
        x ∉ s → y ∉ s → PiNat.cylinder x (PiNat.longestPrefix x s) = PiNat.cylinder y (PiNat.longestPrefix y s)

If two points x, y coincide up to length n, and the longest common prefix of x with s is strictly shorter than n, then the longest common prefix of y with s is the same, and both cylinders of this length based at x and y coincide.

Defined in

Mathlib.Topology.MetricSpace.PiNat

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceDiscreteTopology