induced_mono — Mathlib

English

Let τ1, τ2 be topologies on α with τ1 ≤ τ2, and g: β → α. Then the topology on β induced from τ1 via g is contained in the topology induced from τ2 via g.

Русский

Пусть на α даны топологии τ1, τ2 такие, что τ1 ≤ τ2, и g: β → α. Тогда топология на β, индуцированная τ1 через g, содержится в топологии на β, индуцированной τ2 через g.

LaTeX

$$$\tau_1 \le \tau_2 \implies \operatorname{induced}_g(\tau_1) \le \operatorname{induced}_g(\tau_2)$$$

Lean4

@[gcongr]
theorem induced_mono (h : t₁ ≤ t₂) : t₁.induced g ≤ t₂.induced g :=
  (gc_coinduced_induced g).monotone_u h

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