map_le_map_iff — Mathlib

English

If f is injective, the order between images is equivalent to the order between the preimages.

Русский

Если f инъективно, то порядок между образами эквивалентен порядку между прообразами.

LaTeX

$$$ \text{hf injective} \Rightarrow (N.map f \le N_2.map f) \iff (N \le N_2) $$$

Lean4

theorem map_le_map_iff (hf : Function.Injective f) : N.map f ≤ N₂.map f ↔ N ≤ N₂ :=
  Set.image_subset_image_iff hf

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