comap_le_iff_le_kernMap — Mathlib

English

The relation comap m g ≤ f is equivalent to g ≤ kernMap m f; this expresses a Galois connection between comap and kernMap.

Русский

Отношение comap m g ≤ f эквивалентно g ≤ kernMap m f; это выражает сопряжённость Гало между comap и kernMap.

LaTeX

$$$comap\\ m\\ g \\le f \\iff g \\le kernMap\\ m\\ f$$$

Lean4

theorem comap_le_iff_le_kernMap : comap m g ≤ f ↔ g ≤ kernMap m f := by
  simp [Filter.le_def, mem_comap'', mem_kernMap, -mem_comap]

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