instT0Space — Mathlib

English

If each X_i is a TopologicalSpace and T0, then the space ∀ i, X_i is a T0-space.

Русский

Если каждая X_i — топологическое пространство и T0, то пространствo ∀ i X_i является T0.

LaTeX

$$$\text{If } X_i\ (i\in I)\text{ are Topological spaces with } T0, \; \forall i, X_i\text{ is T0.}$$$

Lean4

instance instT0Space {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, T0Space (X i)] :
    T0Space (∀ i, X i) :=
  ⟨fun _ _ h => funext fun i => (h.map (continuous_apply i)).eq⟩

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