instTopologicalSpace_mono — Mathlib

English

If t ≤ u are topologies on R, then the induced topologies on MvPowerSeries σ R satisfy the same order: a coarser base topology yields a coarser induced topology on power series.

Русский

Если t ≤ u — топологии на R, то полученные индуцированные топологии на MvPowerSeries σ R сохраняют тот же порядок: более грубая (толстая) база порождает более грубую индуцированную топологию на рядовых полиномах.

LaTeX

$$t ≤ u → @instTopologicalSpace σ R t ≤ @instTopologicalSpace σ R u$$

Lean4

theorem instTopologicalSpace_mono (σ : Type*) {R : Type*} {t u : TopologicalSpace R} (htu : t ≤ u) :
    @instTopologicalSpace σ R t ≤ @instTopologicalSpace σ R u :=
  by
  simp only [instTopologicalSpace, Pi.topologicalSpace, le_iInf_iff]
  grw [htu]
  exact iInf_le _

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