English
If B is a topological basis for α and p is a predicate on α, then the collection obtained by restricting B to the subset {x ∈ α | p x} — equivalently the image of B under the inclusion of the subtype — is a topological basis for the subspace {x ∈ α | p x}.
Русский
Если B — топологический базис пространства α, и p — предикат на α, то множество B, ограниченное до подмножества {x ∈ α | p x}, образующееся как изображение B через вложение подтипа, образует базис топологии подпространства {x ∈ α | p x}.
LaTeX
$$$\mathrm{IsTopologicalBasis}\Bigl\{ B \cap \{ x \in \alpha : p(x) \} : B \in \mathcal{B} \Bigr\}$,
where $\mathcal{B}$ is a topological basis for $\alpha$$$
Lean4
theorem isTopologicalBasis_subtype {α : Type*} [TopologicalSpace α] {B : Set (Set α)}
(h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) :
IsTopologicalBasis (Set.preimage (Subtype.val (p := p)) '' B) :=
h.isInducing ⟨rfl⟩
