comap_mono

Mathlib.Topology.UniformSpace.Basic

URI: https://scilib.ai/kg/mathlib#UniformSpace.comap_mono

English

Comap f is monotone: if u ≤ v then u.comap f ≤ v.comap f.

Русский

Обратный образ по f монотонен: если u ≤ v, то u.comap f ≤ v.comap f.

LaTeX

$$Monotone fun u => UniformSpace.comap f u$$

Lean4

theorem comap_mono {α γ} {f : α → γ} : Monotone fun u : UniformSpace γ => u.comap f := fun _ _ hu =>
  Filter.comap_mono hu

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru