le_map_of_comap_le_of_surjective — Mathlib

English

If comap f K ≤ I, then K ≤ map f I. This expresses how the pullback bounds translate forward under a surjective map.

Русский

Если comap f K меньше или равно I, то K меньше или равно map f I.

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall I,K \in \mathrm{Ideal}(S), \; \mathrm{comap}(f) K \le I \Rightarrow K \le \mathrm{map}(f) I$$$

Lean4

theorem le_map_of_comap_le_of_surjective : comap f K ≤ I → K ≤ map f I := fun h =>
  map_comap_of_surjective f hf K ▸ map_mono h

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