map_le_map_iff

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_le_map_iff

English

For injective m, map m f ≤ map m g iff f ≤ g.

Русский

Для инъективной m: map m f ≤ map m g тогда и только тогда f ≤ g.

LaTeX

$$$ map\\ m\\ f \\le map\\ m\\ g \\iff f \\le g $$$

Lean4

theorem map_le_map_iff {f g : Filter α} {m : α → β} (hm : Injective m) : map m f ≤ map m g ↔ f ≤ g := by
  rw [map_le_iff_le_comap, comap_map hm]

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

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

Разделы

Аффилиация

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