r0Space — Mathlib

English

If f: Y → X is an inducing map and X is R0, then Y is R0.

Русский

Если отображение f: Y → X является индуцирующим и X является R0-пространством, то и Y является R0.

LaTeX

$$$R0Space Y \\;\\text{ given }\\; (IsInducing f)\\,,$$$

Lean4

theorem r0Space [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : R0Space Y where
  specializes_symmetric a b := by simpa only [← hf.specializes_iff] using Specializes.symm

Похожие утверждения