Mathlib Map

Theorems · Theorem · general topology

PiNat.isOpen_cylinder

∀ (E : ℕ → Type u_1) [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] (x : (n : ℕ) → E n)
  (n : ℕ), IsOpen (PiNat.cylinder x n)
Defined in
Mathlib.Topology.MetricSpace.PiNat
Cited by
2 results in Mathlib
Foundations
Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceDiscreteTopology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PiNat.isTopologicalBasis_cylinders · cited by 1PiNat.isTopologicalBasis_…CantorScheme.VanishingDiam.map_continuous · cited by 1VanishingDiam.map_continu…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceSetLike.coe · cited by 8199SetLike.coeIsOpen · cited by 2400IsOpenFinset.range · cited by 1341Finset.rangeDiscreteTopology · cited by 373DiscreteTopologyFinset.finite_toSet · cited by 210Finset.finite_toSetisOpen_discrete · cited by 36isOpen_discretePiNat.cylinder · cited by 26PiNat.cylinderisOpen_set_pi · cited by 8isOpen_set_piPiNat.cylinder_eq_pi · cited by 2PiNat.cylinder_eq_piPiNat.isOpen_cylinderCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.