comap_surjective_of_injective — Mathlib

English

If f is injective, comap f is surjective onto Submonoid(N): for every T there exists S with comap f S = T.

Русский

Если f инъективен, то предобраз по f достигает каждого подмономоида: для каждого T существует S, такое что comap_f S = T.

LaTeX

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

Lean4

@[to_additive]
theorem comap_surjective_of_injective : Function.Surjective (comap f) :=
  (gciMapComap hf).u_surjective

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