T0Sierpinski

📁 Source: Mathlib/Topology/ContinuousMap/T0Sierpinski.lean

Statistics

Metric	Count
Definitions productOfMemOpens	1
Theorems eq_induced_by_maps_to_sierpinski, productOfMemOpens_injective, productOfMemOpens_isEmbedding, productOfMemOpens_isInducing	4
Total	5

TopologicalSpace

Definitions

Name	Category	Theorems
productOfMemOpens 📖	CompOp	3 math math: productOfMemOpens_isEmbedding, productOfMemOpens_injective, productOfMemOpens_isInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_induced_by_maps_to_sierpinski 📖	mathematical	—	iInf TopologicalSpace Opens ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice induced SetLike.instMembership Opens.instSetLike sierpinskiSpace	—	le_antisymm le_iInf_iff Continuous.le_induced isOpen_iff_continuous_mem Opens.is_open' generateFrom_iUnion_isOpen isOpen_generateFrom_of_mem isOpen_singleton_true
productOfMemOpens_injective 📖	mathematical	—	DFunLike.coe ContinuousMap Pi.topologicalSpace Opens sierpinskiSpace ContinuousMap.instFunLike productOfMemOpens	—	Inseparable.eq Topology.IsInducing.inseparable_iff productOfMemOpens_isInducing Inseparable.refl
productOfMemOpens_isEmbedding 📖	mathematical	—	Topology.IsEmbedding Pi.topologicalSpace Opens sierpinskiSpace DFunLike.coe ContinuousMap ContinuousMap.instFunLike productOfMemOpens	—	productOfMemOpens_isInducing productOfMemOpens_injective
productOfMemOpens_isInducing 📖	mathematical	—	Topology.IsInducing Pi.topologicalSpace Opens sierpinskiSpace DFunLike.coe ContinuousMap ContinuousMap.instFunLike productOfMemOpens	—	eq_induced_by_maps_to_sierpinski inducing_iInf_to_pi

---

← Back to Index