continuous_map_of_le — Mathlib

English

If s ≤ t are Setoid on α, then the induced map Setoid.map_of_le h is continuous.

Русский

Если s ≤ t — множество эквивалентности на α, то соответствующее отображение Setoid.map_of_le h непрерывно.

LaTeX

$$$ \\operatorname{Continuous}(\\mathrm{Setoid.map\\_of\\_le}(h)). $$$

Lean4

theorem continuous_map_of_le {α : Type*} [TopologicalSpace α] {s t : Setoid α} (h : s ≤ t) :
    Continuous (Setoid.map_of_le h) :=
  continuous_coinduced_rng

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