deltaGenerated_mono — Mathlib

English

If t1 ≤ t2 are topologies on X, then the delta-generated topologies satisfy δGenerated(X, t1) ≤ δGenerated(X, t2).

Русский

Если топологии t1 и t2 на X упорядочены как t1 ≤ t2, то δ-генерируемые топологии удовлетворяют δGenerated(X, t1) ≤ δGenerated(X, t2).

LaTeX

$$$$t_1 \le t_2 \quad\Longrightarrow\quad \deltaGenerated X t_1 \le \deltaGenerated X t_2.$$$$

Lean4

theorem deltaGenerated_mono {X : Type*} {t₁ t₂ : TopologicalSpace X} (h : t₁ ≤ t₂) :
    @deltaGenerated X t₁ ≤ @deltaGenerated X t₂ :=
  by
  rw [← continuous_id_iff_le,
    @continuous_to_deltaGenerated _ _ (@deltaGenerated X t₁) t₂ deltaGeneratedSpace_deltaGenerated id]
  exact continuous_id_iff_le.2 <| (@deltaGenerated_le X t₁).trans h

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