Theorems · Theorem · general topology

DiscreteTopology.of_subset

∀ {X : Type u_5} [inst : TopologicalSpace X] {s t : Set X}, DiscreteTopology ↑s → t ⊆ s → DiscreteTopology ↑t

Let s, t ⊆ X be two subsets of a topological space X. If t ⊆ s and the topology induced by X on s is discrete, then also the topology induces on t is discrete. (Compare IsDiscrete.mono which is the same thing stated without using subtypes.)

Defined in

Mathlib.Topology.Constructions

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace