map_le_iff_le_comap — Mathlib

English

Let f be a map. Then the map along f and the comap along f form a Galois connection: s.map f ≤ t iff s ≤ t.comap f.

Русский

Пусть f — отображение. Тогда отображение через f и обратное через f образуют Галуа-соединение: s.map f ≤ t ⇔ s ≤ t.comap f.

LaTeX

$$$ s.map f \le t \;\Longleftrightarrow\; s \le t.comap f $$$

Lean4

theorem map_le_iff_le_comap {f : F} {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} :
    s.map f ≤ t ↔ s ≤ t.comap f :=
  Set.image_subset_iff

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