comap_injective — Mathlib

English

If f is surjective, comap f is injective on filters: comap f is injective.

Русский

Если отображение сюръективно, то операция обратного изображения по f инъективна на фильтрах.

LaTeX

$$$ \\text{comap}_f \\text{ is injective when } f \\text{ is surjective}$$$

Lean4

theorem comap_injective {f : α → β} (hf : Surjective f) : Injective (comap f) :=
  LeftInverse.injective <| map_comap_of_surjective hf

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