coinduced_mono — Mathlib

English

Let τ1 ≤ τ2 be topologies on α and f: α → β. Then the coinduced topologies on β satisfy τ1.coinduced f ≤ τ2.coinduced f.

Русский

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

LaTeX

$$$t_1 \le t_2 \implies t_1.coinduced f \le t_2.coinduced f$$$

Lean4

@[gcongr]
theorem coinduced_mono (h : t₁ ≤ t₂) : t₁.coinduced f ≤ t₂.coinduced f :=
  (gc_coinduced_induced f).monotone_l h

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